# HG changeset patch
# User kleing
# Date 1021142431 -7200
# Node ID 94648e0e4506fcbe311e4fb19fabf49f129e904a
# Parent  6568fee2bd3adbc84cf1035f9dc7f02669e11c1d
fix for change in nat number simplification

diff -r 6568fee2bd3a -r 94648e0e4506 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sat May 11 20:27:13 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat May 11 20:40:31 2002 +0200
@@ -253,6 +253,8 @@
    (                                    [], [Class list_name, Class list_name]),
    (                          [PrimT Void], [Class list_name, Class list_name])]"
 
+declare nat_number [simp]
+
 lemma wt_append [simp]:
   "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
              [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
@@ -348,7 +350,9 @@
   Phi :: prog_type ("\<Phi>")
   "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
              if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
-  
+
+declare nat_number [simp del]   
+
 lemma wf_prog:
   "wt_jvm_prog E \<Phi>" 
   apply (unfold wt_jvm_prog_def)