✐‹creator "Kevin Kappelmann"› subsection ‹Fact Tactic› theory Unify_Fact_Tactic_Base imports Unify_Resolve_Tactics_Base begin paragraph ‹Summary› text ‹Fact tactic with adjustable unifier.› ML_file‹unify_fact_base.ML› ML_file‹unify_fact.ML› end