src/HOL/Nat.thy
changeset 54223 85705ba18add
parent 54222 24874b4024d1
child 54411 f72e58a5a75f
     1.1 --- a/src/HOL/Nat.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -369,8 +369,8 @@
     1.4  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
     1.5  
     1.6  declare less_eq_nat.simps [simp del]
     1.7 -lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps)
     1.8  lemma le0 [iff]: "0 \<le> (n\<Colon>nat)" by (simp add: less_eq_nat.simps)
     1.9 +lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by simp
    1.10  
    1.11  definition less_nat where
    1.12    less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"