# HG changeset patch
# User kleing
# Date 1021372422 -7200
# Node ID fe118a977a6dd02a2b6b7ebcec9e2f4bace014fa
# Parent  491a48cf602338c84dfc2e4941ce4b72c692f60c
numerals work again

diff -r 491a48cf6023 -r fe118a977a6d src/HOL/MicroJava/BV/BVExample.thy
--- 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)