--- 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)