--- a/src/HOL/ex/Unification.thy Tue Aug 23 17:43:06 2011 +0200
+++ b/src/HOL/ex/Unification.thy Tue Aug 23 17:44:31 2011 +0200
@@ -11,10 +11,10 @@
begin
text {*
- Implements Manna & Waldinger's formalization, with Paulson's
+ Implements Manna \& Waldinger's formalization, with Paulson's
simplifications, and some new simplifications by Slind and Krauss.
- Z Manna & R Waldinger, Deductive Synthesis of the Unification
+ Z Manna \& R Waldinger, Deductive Synthesis of the Unification
Algorithm. SCP 1 (1981), 5-48
L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5