--- a/src/HOL/List.thy Thu Apr 27 15:06:42 2006 +0200
+++ b/src/HOL/List.thy Thu Apr 27 17:40:17 2006 +0200
@@ -1420,6 +1420,22 @@
apply (case_tac j, auto)
done
+lemma take_zip:
+ "!!xs ys. take n (zip xs ys) = zip (take n xs) (take n ys)"
+apply (induct n)
+ apply simp
+apply (case_tac xs, simp)
+apply (case_tac ys, simp_all)
+done
+
+lemma drop_zip:
+ "!!xs ys. drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
+apply (induct n)
+ apply simp
+apply (case_tac xs, simp)
+apply (case_tac ys, simp_all)
+done
+
subsubsection {* @{text list_all2} *}