src/HOL/MicroJava/BV/Effect.thy

--- a/src/HOL/MicroJava/BV/Effect.thy	Wed Aug 17 11:15:23 2005 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Aug 17 11:44:02 2005 +0200
@@ -401,10 +401,6 @@
   by (auto simp add: eff_def xcpt_eff_def norm_eff_def)
 
 
-text {* some helpers to make the specification directly executable: *}
-declare list_all2_Nil [code]
-declare list_all2_Cons [code]
-
 lemma xcpt_app_lemma [code]:
   "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))"
   by (simp add: list_all_iff)