Theory Unify_Resolve_Tactics_Base

✐‹creator "Kevin Kappelmann"›
subsection ‹Resolution Tactics›
theory Unify_Resolve_Tactics_Base
  imports
    Unify_Assumption_Tactic_Base
    ML_Unifiers_Base
    ML_Method_Utils
begin

paragraph ‹Summary›
text ‹Resolution tactics and methods with adjustable unifier.›

ML_file‹unify_resolve_base.ML›
ML_file‹unify_resolve.ML›

end