src/HOL/Code_Numeral.thy

--- a/src/HOL/Code_Numeral.thy	Wed May 27 07:56:11 2009 +0200
+++ b/src/HOL/Code_Numeral.thy	Wed May 27 22:11:05 2009 +0200
@@ -215,7 +215,13 @@
   "of_nat n < of_nat m \<longleftrightarrow> n < m"
   by simp
 
-lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp
+lemma code_numeral_zero_minus_one:
+  "(0::code_numeral) - 1 = 0"
+  by simp
+
+lemma Suc_code_numeral_minus_one:
+  "Suc_code_numeral n - 1 = n"
+  by simp
 
 lemma of_nat_code [code]:
   "of_nat = Nat.of_nat"