✐‹creator "Kevin Kappelmann"› subsection ‹Assumption Tactic› theory Unify_Assumption_Tactic_Base imports ML_Functor_Instances ML_Tactic_Utils ML_Unification_Parsers begin paragraph ‹Summary› text ‹Assumption tactic and method with adjustable unifier.› ML_file‹unify_assumption_base.ML› ML_file‹unify_assumption.ML› end