src/HOL/W0/W0.thy
changeset 12961 cd4f8d5c6450
parent 12945 95853fbcc718
child 13537 f506eb568121
     1.1 --- a/src/HOL/W0/W0.thy	Tue Feb 26 21:47:33 2002 +0100
     1.2 +++ b/src/HOL/W0/W0.thy	Tue Feb 26 21:57:13 2002 +0100
     1.3 @@ -426,7 +426,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -section {* Correctness and completeness of the type inference algorithm @{text \<W>} *}
     1.8 +section {* Correctness and completeness of the type inference algorithm W *}
     1.9  
    1.10  consts
    1.11    W :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<W>")
    1.12 @@ -785,7 +785,7 @@
    1.13    done
    1.14  
    1.15  
    1.16 -section {* Equivalence of @{text \<W>} and @{text \<I>} *}
    1.17 +section {* Equivalence of W and I *}
    1.18  
    1.19  text {*
    1.20    Recursive definition of type inference algorithm @{text \<I>} for