✐‹creator "Kevin Kappelmann"› section ‹ML Unification Basics› theory ML_Unification_Base imports ML_Logger ML_Binders ML_Normalisations ML_Theorem_Utils SpecCheck.SpecCheck_Show begin paragraph ‹Summary› text ‹Basic definitions and utilities for unification algorithms.› ML_file‹unification_base.ML› ML_file‹unification_util.ML› end