numerals work again
authorkleing
Tue May 14 12:33:42 2002 +0200 (2002-05-14)
changeset 13148fe118a977a6d
parent 13147 491a48cf6023
child 13149 773657d466cb
numerals work again
src/HOL/MicroJava/BV/BVExample.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon May 13 15:45:21 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue May 14 12:33:42 2002 +0200
     1.3 @@ -253,8 +253,6 @@
     1.4     (                                    [], [Class list_name, Class list_name]),
     1.5     (                          [PrimT Void], [Class list_name, Class list_name])]"
     1.6  
     1.7 -declare nat_number [simp]
     1.8 -
     1.9  lemma wt_append [simp]:
    1.10    "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
    1.11               [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
    1.12 @@ -351,8 +349,6 @@
    1.13    "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
    1.14               if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
    1.15  
    1.16 -declare nat_number [simp del]   
    1.17 -
    1.18  lemma wf_prog:
    1.19    "wt_jvm_prog E \<Phi>" 
    1.20    apply (unfold wt_jvm_prog_def)