Theory ML_Unifiers_Base

✐‹creator "Kevin Kappelmann"›
section ‹ML Unifiers›
theory ML_Unifiers_Base
  imports
    ML_Unification_Base
    ML_Tactic_Utils
begin
(*TODO: make all sequence computations lazy*)
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›

paragraph ‹Unification via Tactics›

ML_file‹tactic_unification.ML›

end