src/HOL/ex/Unification.thy
```     1.1 --- a/src/HOL/ex/Unification.thy	Sun Jun 03 23:16:46 2007 +0200
1.2 +++ b/src/HOL/ex/Unification.thy	Sun Jun 03 23:16:47 2007 +0200
1.3 @@ -4,9 +4,9 @@
1.4
1.5  header {* Case study: Unification Algorithm *}
1.6
1.7 -(*<*)theory Unification
1.8 +theory Unification
1.9  imports Main
1.10 -begin(*>*)
1.11 +begin
1.12
1.13  text {*
1.14    This is a formalization of a first-order unification
1.15 @@ -15,7 +15,7 @@
1.16
1.17    This is basically a modernized version of a previous formalization
1.18    by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
1.19 -  previous work by Paulson and Manna @{text "&"} Waldinger (for details, see
1.20 +  previous work by Paulson and Manna \& Waldinger (for details, see
1.21    there).
1.22
1.23    Unlike that formalization, where the proofs of termination and
1.24 @@ -23,6 +23,7 @@
1.25    partial correctness and termination separately.
1.26  *}
1.27
1.28 +
1.29  subsection {* Basic definitions *}
1.30
1.31  datatype 'a trm =
1.32 @@ -62,6 +63,7 @@
1.33  where
1.34    "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2"
1.35
1.36 +
1.37  subsection {* Basic lemmas *}
1.38
1.39  lemma apply_empty[simp]: "t \<triangleleft> [] = t"
1.40 @@ -105,6 +107,7 @@
1.41  lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
1.42    by auto
1.43
1.44 +
1.45  subsection {* Specification: Most general unifiers *}
1.46
1.47  definition
1.48 @@ -492,7 +495,6 @@
1.49
1.50  subsection {* Termination proof *}
1.51
1.52 -
1.53  termination unify
1.54  proof
1.55    let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
1.56 @@ -532,23 +534,4 @@
1.57    qed
1.58  qed
1.59
1.60 -
1.61 -(*<*)end(*>*)
1.62 -
1.63 -
1.64 -
1.65 -
1.66 -
1.67 -
1.68 -
1.69 -
1.70 -
1.71 -
1.72 -
1.73 -
1.74 -
1.75 -
1.76 -
1.77 -
1.78 -
1.79 -
1.80 +end
```