# HG changeset patch
# User oheimb
# Date 991320604 -7200
# Node ID fedccaeb52675d85e44535a557d7bbc0acbe26c4
# Parent  c150861633da510994f7103996f18f8ee2b5f612
added list_all2_trans

diff -r c150861633da -r fedccaeb5267 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu May 31 16:17:28 2001 +0200
+++ b/src/HOL/List.ML	Thu May 31 16:50:04 2001 +0200
@@ -1125,7 +1125,19 @@
 by (force_tac (claset(), simpset() addsimps [set_zip]) 1);
 qed "list_all2_conv_all_nth";
 
-(** foldl **)
+Goal "ALL a b c. P1 a b --> P2 b c --> P3 a c ==> \
+\ ALL bs cs. list_all2 P1 as bs --> list_all2 P2 bs cs --> list_all2 P3 as cs";
+by (induct_tac "as" 1);
+by  (Simp_tac 1);
+by (rtac allI 1);
+by (induct_tac "bs" 1);
+by  (Simp_tac 1);
+by (rtac allI 1);
+by (induct_tac "cs" 1);
+by Auto_tac;
+qed_spec_mp "list_all2_trans";
+
+
 section "foldl";
 
 Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";