src/HOL/MicroJava/BV/BVExample.thy
changeset 13043 ad1828b479b7
parent 13006 51c5f3f11d16
child 13052 3bf41c474a88
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Thu Mar 07 23:21:19 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Mar 07 23:41:30 2002 +0100
     1.3 @@ -314,7 +314,7 @@
     1.4  lemma wt_makelist [simp]:
     1.5    "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
     1.6    apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
     1.7 -  apply (simp add: wt_start_def nat_number_of)
     1.8 +  apply (simp add: wt_start_def nat_number)
     1.9    apply (simp add: wt_instr_def)
    1.10    apply clarify
    1.11    apply (elim pc_end pc_next pc_0)