src/HOL/Nat_Numeral.thy

--- a/src/HOL/Nat_Numeral.thy	Wed May 05 16:46:19 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy	Wed May 05 16:53:21 2010 +0200
@@ -687,6 +687,13 @@
 lemmas nat_number' =
   nat_number_of_Bit0 nat_number_of_Bit1
 
+lemmas nat_arith =
+  add_nat_number_of
+  diff_nat_number_of
+  mult_nat_number_of
+  eq_nat_number_of
+  less_nat_number_of
+
 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   by (fact Let_def)