--- a/src/HOL/Nat_Numeral.thy Thu May 06 17:59:20 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy Thu May 06 18:16:07 2010 +0200
@@ -694,6 +694,13 @@
eq_nat_number_of
less_nat_number_of
+lemmas semiring_norm =
+ Let_def arith_simps nat_arith rel_simps neg_simps if_False
+ if_True add_0 add_Suc add_number_of_left mult_number_of_left
+ numeral_1_eq_1 [symmetric] Suc_eq_plus1
+ numeral_0_eq_0 [symmetric] numerals [symmetric]
+ iszero_simps not_iszero_Numeral1
+
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
by (fact Let_def)