--- a/src/HOL/MicroJava/BV/BVExample.thy Mon May 13 15:45:21 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Tue May 14 12:33:42 2002 +0200
@@ -253,8 +253,6 @@
( [], [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"
@@ -351,8 +349,6 @@
"\<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)