# HG changeset patch
# User wenzelm
# Date 1014757033 -3600
# Node ID cd4f8d5c645088e1b51bb07bada2e853a67e4d44
# Parent  e4b2c9d3bf4be3b5236e506eeb58e21dd407ba68
tuned;

diff -r e4b2c9d3bf4b -r cd4f8d5c6450 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Tue Feb 26 21:47:33 2002 +0100
+++ b/src/HOL/W0/W0.thy	Tue Feb 26 21:57:13 2002 +0100
@@ -426,7 +426,7 @@
 qed
 
 
-section {* Correctness and completeness of the type inference algorithm @{text \<W>} *}
+section {* Correctness and completeness of the type inference algorithm W *}
 
 consts
   W :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<W>")
@@ -785,7 +785,7 @@
   done
 
 
-section {* Equivalence of @{text \<W>} and @{text \<I>} *}
+section {* Equivalence of W and I *}
 
 text {*
   Recursive definition of type inference algorithm @{text \<I>} for