--- 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