added pointer to new Unification theory
authorkrauss
Thu May 17 22:37:34 2007 +0200 (2007-05-17)
changeset 230006f158bba99e4
parent 22999 c1ce129e6f9c
child 23001 3608f0362a91
added pointer to new Unification theory
src/HOL/Subst/Unify.thy
     1.1 --- a/src/HOL/Subst/Unify.thy	Thu May 17 22:33:41 2007 +0200
     1.2 +++ b/src/HOL/Subst/Unify.thy	Thu May 17 22:37:34 2007 +0200
     1.3 @@ -10,8 +10,12 @@
     1.4  imports Unifier
     1.5  begin
     1.6  
     1.7 -text{*
     1.8 -Substitution and Unification in Higher-Order Logic.
     1.9 +subsection {* Substitution and Unification in Higher-Order Logic. *}
    1.10 +
    1.11 +text {*
    1.12 +NB: This theory is already quite old.
    1.13 +You might want to look at the newer Isar formalization of
    1.14 +unification in HOL/ex/Unification.thy.
    1.15  
    1.16  Implements Manna and Waldinger's formalization, with Paulson's simplifications,
    1.17  and some new simplifications by Slind.