✐‹creator "Kevin Kappelmann"› subsection ‹Metis› theory Extended_Metis_Data imports HOL.Metis ML_Unification.ML_Functor_Instances ML_Unification.ML_Logger SpecCheck.SpecCheck_Show begin ML_file‹extended_metis_data.ML› end