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