# HG changeset patch
# User haftmann
# Date 1243455065 -7200
# Node ID 55e70b6d812ec7dafce7e6b92ebf6f36f171c27d
# Parent  2662d1cdc51f16b061182cf8572036b5649a6cb4
added lemma about 0 - 1

diff -r 2662d1cdc51f -r 55e70b6d812e 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"