✐‹creator "Kevin Kappelmann"› section ‹ML Unifiers› theory ML_Unifiers_Base imports ML_Unification_Base begin paragraph ‹Summary› text ‹Unification modulo equations and combinators for unifiers.› paragraph ‹Combinators› ML_file‹unification_combinator.ML› paragraph ‹Type Unifiers› ML_file‹type_unification.ML› paragraph ‹Standard Unifiers› ML_file‹higher_order_unification.ML› ML_file‹higher_order_pattern_unification.ML› ML_file‹first_order_unification.ML› end