Theory ML_Unification.ML_Unification_Hints_Base

✐‹creator "Kevin Kappelmann"›
section ‹Unification Hints›
theory ML_Unification_Hints_Base
  imports
    ML_Conversion_Utils
    ML_Functor_Instances
    ML_Generic_Data_Utils
    ML_Priorities
    ML_Term_Index
    ML_Tactic_Utils
    ML_Term_Utils
    ML_Unifiers_Base
    ML_Unification_Parsers
begin

paragraph ‹Summary›
text ‹A generalisation of unification hints, originally introduced in \<^cite>‹"unif-hints"›.
We support a generalisation that
▸ allows additional universal variables in premises
▸ allows non-atomic left-hand sides for premises
▸ allows arbitrary functions to perform the matching/unification of a hint with a disagreement pair.

General shape of a hint:
‹⋀y1...yn. (⋀x1...xn1. lhs1 ≡ rhs1) ⟹ ... ⟹ (⋀x1...xnk. lhsk ≡ rhsk) ⟹ lhs ≡ rhs›
›

ML_file‹unification_hints_base.ML›
ML_file‹unification_hints.ML›
ML_file‹term_index_unification_hints.ML›

end