# 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 \ (\loc. v = Addr loc))" by (cases v) (auto simp add: isRef_def) - -(* fixme: move to List.thy *) -lemma list_all2I: - "\x \ set (zip a b). split P x \ length a = length b \ list_all2 P a b" - by (simp add: list_all2_def) - - lemma app'Store[simp]: "app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (\T ST'. ST = T#ST' \ idx < length LT)" by (cases ST, auto)