✐‹creator "Kevin Kappelmann"› section ‹Unification Attributes› theory Unification_Attributes_Base imports Unify_Resolve_Tactics_Base begin paragraph ‹Summary› text ‹OF attribute with adjustable unifier.› ML_file‹unify_of_base.ML› ML_file‹unify_of.ML› end