fix for change in nat number simplification
authorkleing
Sat May 11 20:40:31 2002 +0200 (2002-05-11)
changeset 1313994648e0e4506
parent 13138 6568fee2bd3a
child 13140 6d97dbb189a9
fix for change in nat number simplification
src/HOL/MicroJava/BV/BVExample.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Sat May 11 20:27:13 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat May 11 20:40:31 2002 +0200
     1.3 @@ -253,6 +253,8 @@
     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 @@ -348,7 +350,9 @@
    1.13    Phi :: prog_type ("\<Phi>")
    1.14    "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
    1.15               if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
    1.16 -  
    1.17 +
    1.18 +declare nat_number [simp del]   
    1.19 +
    1.20  lemma wf_prog:
    1.21    "wt_jvm_prog E \<Phi>" 
    1.22    apply (unfold wt_jvm_prog_def)