src/HOL/Library/Char_ord.thy
changeset 37765 26bdfb7b680b
parent 30663 0b6aff7451b2
child 48926 8d7778a19857
--- a/src/HOL/Library/Char_ord.thy	Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Char_ord.thy	Mon Jul 12 08:58:13 2010 +0200
@@ -63,11 +63,11 @@
 begin
 
 definition
-  char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+  char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
     n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
 
 definition
-  char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+  char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
     n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
 
 instance