src/HOL/ex/Unification.thy
changeset 44428 ccb8998f70b7
parent 44373 7321d628b57d
child 56790 f54097170704
     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