src/HOL/ex/Unification.thy
changeset 23219 87ad6e8a5f2c
parent 23024 70435ffe077d
child 23373 ead82c82da9e
--- a/src/HOL/ex/Unification.thy	Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/Unification.thy	Sun Jun 03 23:16:47 2007 +0200
@@ -4,9 +4,9 @@
 
 header {* Case study: Unification Algorithm *}
 
-(*<*)theory Unification
+theory Unification
 imports Main
-begin(*>*)
+begin
 
 text {* 
   This is a formalization of a first-order unification
@@ -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 @{text "&"} Waldinger (for details, see
+  previous work by Paulson and Manna \& Waldinger (for details, see
   there).
 
   Unlike that formalization, where the proofs of termination and
@@ -23,6 +23,7 @@
   partial correctness and termination separately.
 *}
 
+
 subsection {* Basic definitions *}
 
 datatype 'a trm = 
@@ -62,6 +63,7 @@
 where
   "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" 
 
+
 subsection {* Basic lemmas *}
 
 lemma apply_empty[simp]: "t \<triangleleft> [] = t"
@@ -105,6 +107,7 @@
 lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
   by auto
 
+
 subsection {* Specification: Most general unifiers *}
 
 definition
@@ -492,7 +495,6 @@
 
 subsection {* Termination proof *}
 
-
 termination unify
 proof 
   let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
@@ -532,23 +534,4 @@
   qed
 qed
 
-
-(*<*)end(*>*)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+end