1.1 --- a/src/HOL/Code_Numeral.thy	Wed May 27 07:56:11 2009 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed May 27 22:11:05 2009 +0200
     1.3 @@ -215,7 +215,13 @@
     1.4    "of_nat n < of_nat m \<longleftrightarrow> n < m"
     1.5    by simp
     1.6  
     1.7 -lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp
     1.8 +lemma code_numeral_zero_minus_one:
     1.9 +  "(0::code_numeral) - 1 = 0"
    1.10 +  by simp
    1.11 +
    1.12 +lemma Suc_code_numeral_minus_one:
    1.13 +  "Suc_code_numeral n - 1 = n"
    1.14 +  by simp
    1.15  
    1.16  lemma of_nat_code [code]:
    1.17    "of_nat = Nat.of_nat"