src/HOL/Nat_Numeral.thy

--- a/src/HOL/Nat_Numeral.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -693,11 +693,7 @@
 apply (simp only: nat_add_distrib, simp)
 done
 
-lemmas nat_number =
-  nat_number_of_Pls nat_number_of_Min
-  nat_number_of_Bit0 nat_number_of_Bit1
-
-lemmas nat_number' =
+lemmas eval_nat_numeral =
   nat_number_of_Bit0 nat_number_of_Bit1
 
 lemmas nat_arith =