renamed nat_number_of to nat_number (avoid clash with separate theorem);

--- a/src/HOL/Integ/NatBin.thy	Thu Mar 07 23:21:19 2002 +0100
+++ b/src/HOL/Integ/NatBin.thy	Thu Mar 07 23:41:30 2002 +0100
@@ -52,7 +52,7 @@
   apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc)
   done
 
-lemmas nat_number_of =
+lemmas nat_number =
   nat_number_of_Pls nat_number_of_Min
   nat_number_of_BIT_True nat_number_of_BIT_False
 

--- a/src/HOL/MicroJava/BV/BVExample.thy	Thu Mar 07 23:21:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Mar 07 23:41:30 2002 +0100
@@ -314,7 +314,7 @@
 lemma wt_makelist [simp]:
   "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
   apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
-  apply (simp add: wt_start_def nat_number_of)
+  apply (simp add: wt_start_def nat_number)
   apply (simp add: wt_instr_def)
   apply clarify
   apply (elim pc_end pc_next pc_0)