renamed nat_number_of to nat_number (avoid clash with separate theorem);
authorwenzelm
Thu, 07 Mar 2002 23:41:30 +0100
changeset 13043 ad1828b479b7
parent 13042 d8a345d9e067
child 13044 c049910774cb
renamed nat_number_of to nat_number (avoid clash with separate theorem);
src/HOL/Integ/NatBin.thy
src/HOL/MicroJava/BV/BVExample.thy
--- 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)