# HG changeset patch
# User paulson
# Date 1077183628 -3600
# Node ID cc96cc06abf9d112674c174cc8d93703a45a603e
# Parent  51b24127eef2124119390a6bce5cd1789049f2a0
new theorem

diff -r 51b24127eef2 -r cc96cc06abf9 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 19 10:37:15 2004 +0100
+++ b/src/HOL/List.thy	Thu Feb 19 10:40:28 2004 +0100
@@ -1132,6 +1132,10 @@
   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
   by (simp add: list_all2_conv_all_nth)
 
+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 list_all2_nthD:
   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   by (simp add: list_all2_conv_all_nth)