✐‹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