src/HOL/ex/Unification.thy

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