# HG changeset patch
# User paulson
# Date 1077183692 -3600
# Node ID b3b15305a1c9649aaefc62f0c7391d4198547697
# Parent  011a2a49d3033994f70a43f0e75a385375c4d12b
moved list_all2I to List.thy

diff -r 011a2a49d303 -r b3b15305a1c9 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Feb 19 10:41:01 2004 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Feb 19 10:41:32 2004 +0100
@@ -20,13 +20,6 @@
   "isRef v = (v = Null \<or> (\<exists>loc. v = Addr loc))"
   by (cases v) (auto simp add: isRef_def)
 
-
-(* fixme: move to List.thy *)
-lemma list_all2I:
-  "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
-  by (simp add: list_all2_def)
-
-
 lemma app'Store[simp]:
   "app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST' \<and> idx < length LT)"
   by (cases ST, auto)