1.1 --- a/src/HOL/ex/Unification.thy	Sat May 19 11:33:28 2007 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Sat May 19 11:33:30 2007 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5    This is basically a modernized version of a previous formalization
     1.6    by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
     1.7 -  previous work by Paulson and Manna & Waldinger (for details, see
     1.8 +  previous work by Paulson and Manna @{text "&"} Waldinger (for details, see
     1.9    there).
    1.10  
    1.11    Unlike that formalization, where the proofs of termination and