# HG changeset patch
# User huffman
# Date 1315759218 25200
# Node ID 02efd5a6b6e5d3f71913dd4313de4b776acc3ea4
# Parent  a7f9c97378b3f1b41c94dfa7efc0d10506fd201e
tuned proofs

diff -r a7f9c97378b3 -r 02efd5a6b6e5 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Sun Sep 11 07:21:45 2011 -0700
+++ b/src/HOL/Nat_Numeral.thy	Sun Sep 11 09:40:18 2011 -0700
@@ -334,10 +334,10 @@
 by (simp add: nat_number_of_def)
 
 lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
-by (simp add: nat_number_of_def)
+  by (rule semiring_numeral_0_eq_0)
 
 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
-by (simp add: nat_number_of_def)
+  by (rule semiring_numeral_1_eq_1)
 
 lemma Numeral1_eq1_nat:
   "(1::nat) = Numeral1"
@@ -354,7 +354,7 @@
          (if neg (number_of v :: int) then 0  
           else (number_of v :: int))"
   unfolding nat_number_of_def number_of_is_id neg_def
-  by simp
+  by simp (* FIXME: redundant with of_nat_number_of_eq *)
 
 lemma nonneg_int_cases:
   fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"