Theory Zippy_Goal_Pos_Updates

✐‹creator "Kevin Kappelmann"›
theory Zippy_Goal_Pos_Updates
  imports
    Generic_Table_Data
    Zippy_Actions
    Zippy_Action_Clusters
    Zippy_Goal_Pos_Updates_Base
    Zippy_Goals
begin

ML_file‹zippy_goals_pos_mixin_base.ML›
ML_file‹zippy_goals_pos_mixin.ML›

(*ground polymorphic types since only ground types can be stored in the generic context.*)
setup‹Context.theory_map ML_Gen.ground_zipper_types›
ML_file‹zippy_update_goal_cluster_mixin_base.ML›
ML_file‹zippy_update_goal_cluster_mixin.ML›
(*reset grounding*)
setup‹Context.theory_map ML_Gen.reset_zipper_types›

ML_file‹zippy_goals_pos_copy_mixin_base.ML›
ML_file‹zippy_goals_pos_copy_mixin.ML›

end