# HG changeset patch
# User haftmann
# Date 1179567210 -7200
# Node ID 70435ffe077da78360509df98c920b1aa3c80b64
# Parent  7b52c4fde622eb4b4402654276b8524d1f311084
fixed text

diff -r 7b52c4fde622 -r 70435ffe077d 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