src/HOL/Library/Char_ord.thy
changeset 28562 4e74209f113e
parent 27682 25aceefd4786
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/Char_ord.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -64,11 +64,11 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  char_less_eq_def [code func 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 [code del]: "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 func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.13 +  char_less_def [code del]: "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
    1.17 @@ -90,7 +90,7 @@
    1.18  
    1.19  end
    1.20  
    1.21 -lemma [simp, code func]:
    1.22 +lemma [simp, code]:
    1.23    shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    1.24    and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    1.25    unfolding char_less_eq_def char_less_def by simp_all