# HG changeset patch
# User wenzelm
# Date 1015540890 -3600
# Node ID ad1828b479b795bfafd13cb8769adb66dd218035
# Parent  d8a345d9e067858b750d662f1e9a11a19fce54f6
renamed nat_number_of to nat_number (avoid clash with separate theorem);

diff -r d8a345d9e067 -r ad1828b479b7 src/HOL/Integ/NatBin.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
 
diff -r d8a345d9e067 -r ad1828b479b7 src/HOL/MicroJava/BV/BVExample.thy
--- 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)