# HG changeset patch
# User kleing
# Date 1008458238 -3600
# Node ID 3fb416265ba978725b40a83288e4796abc8108a3
# Parent  4bdbc5a977f605fae57d8a3565f3398fe5368172
list_all2_rev

diff -r 4bdbc5a977f6 -r 3fb416265ba9 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Dec 14 22:32:52 2001 +0100
+++ b/src/HOL/List.ML	Sun Dec 16 00:17:18 2001 +0100
@@ -1092,6 +1092,12 @@
 qed "list_all2_Cons2";
 
 Goalw [list_all2_def]
+ "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys";
+by (asm_full_simp_tac (simpset() addsimps [zip_rev] addcongs [conj_cong]) 1);
+qed "list_all2_rev";
+AddIffs[list_all2_rev];
+
+Goalw [list_all2_def]
  "list_all2 P (xs@ys) zs = \
 \ (EX us vs. zs = us@vs & length us = length xs & length vs = length ys & \
 \            list_all2 P xs us & list_all2 P ys vs)";