fixed document;
authorwenzelm
Tue Aug 23 17:44:31 2011 +0200 (2011-08-23)
changeset 44428ccb8998f70b7
parent 44427 c4a86d72a5cc
child 44429 e5506cfe1b5a
fixed document;
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/ex/Unification.thy	Tue Aug 23 17:43:06 2011 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Tue Aug 23 17:44:31 2011 +0200
     1.3 @@ -11,10 +11,10 @@
     1.4  begin
     1.5  
     1.6  text {* 
     1.7 -  Implements Manna & Waldinger's formalization, with Paulson's
     1.8 +  Implements Manna \& Waldinger's formalization, with Paulson's
     1.9    simplifications, and some new simplifications by Slind and Krauss.
    1.10  
    1.11 -  Z Manna & R Waldinger, Deductive Synthesis of the Unification
    1.12 +  Z Manna \& R Waldinger, Deductive Synthesis of the Unification
    1.13    Algorithm.  SCP 1 (1981), 5-48
    1.14  
    1.15    L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5