Theory TD_Interface

theory TD_Interface
  imports
    TD0
    TD_plain
    TD_plain_s
    TD_plain_s_warrow
    TD_plain_widen
    TD
    TD_widen
    TD_warrow
    TD_wn_phases
    TD_wn_post
    TD_wn_wo_opt
    TD_wn_post_wo_opt
    Worklist
begin

text ‹Entry point for theories building on the solvers without side effects;
  🗏‹TD_side_Interface.thy› is the counterpart for the side-effecting ones. Record fields
  are global constants, so a field named like a common variable would capture every
  downstream variable of that name. The fields below keep their paper names inside this
  session; importing this theory hides the short names, and the qualified names
  (e.g.\ ‹TD_plain.state.σ›) remain.›

hide_const (open)
  TD_plain.state.σ TD_plain.state.σ_update
  TD_wn_phases.state.point TD_wn_phases.state.point_update
  TD_warrow.post_state.post TD_warrow.post_state.post_update
  Worklist.W

end