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