--- a/src/HOL/Subst/Unify.thy Thu May 17 22:33:41 2007 +0200
+++ b/src/HOL/Subst/Unify.thy Thu May 17 22:37:34 2007 +0200
@@ -10,8 +10,12 @@
imports Unifier
begin
-text{*
-Substitution and Unification in Higher-Order Logic.
+subsection {* Substitution and Unification in Higher-Order Logic. *}
+
+text {*
+NB: This theory is already quite old.
+You might want to look at the newer Isar formalization of
+unification in HOL/ex/Unification.thy.
Implements Manna and Waldinger's formalization, with Paulson's simplifications,
and some new simplifications by Slind.