Theory TD.TD_side_Interface

theory TD_side_Interface
  imports TD_side_upd_rule
begin

text ‹Entry point for theories building on the side-effecting solvers;
  🗏‹TD_Interface.thy› is the counterpart for the others. 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_side.state.σ›,
  ‹ug_state.ρ›) remain.›

hide_const (open)
  TD_side.state.σ TD_side.state.σ_update
  Update_rules.ug_state.ρ Update_rules.ug_state.ρ_update
  Update_rules.ug_state_with_gas.gas Update_rules.ug_state_with_gas.gas_update
  TD_side_upd_rule.state.point TD_side_upd_rule.state.point_update

end