# HG changeset patch
# User krauss
# Date 1179434254 -7200
# Node ID 6f158bba99e4539165fc4424dc37cf7e82684b87
# Parent  c1ce129e6f9c6ac007dc06ddca91bded6d37f082
added pointer to new Unification theory

diff -r c1ce129e6f9c -r 6f158bba99e4 src/HOL/Subst/Unify.thy
--- 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.