Theory Zippy_Instance_Hom_Changed_Goals_Data

✐‹creator "Kevin Kappelmann"›
subsection ‹Homogenously Changed Goals Data›
theory Zippy_Instance_Hom_Changed_Goals_Data
  imports
    Generic_Term_Index_Data
    Zippy_Instance
begin

(*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_instance_hom_changed_goals_data.ML›
(*reset grounding*)
setup‹Context.theory_map ML_Gen.reset_zipper_types›

end