# HG changeset patch
# User nipkow
# Date 920897354 -3600
# Node ID 81e7fbf61db26969b1f29a7af6adf4db166bcd92
# Parent  4cbdb974220c6ce44850ba0c3522c49c4e7659f9
modified zip

diff -r 4cbdb974220c -r 81e7fbf61db2 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Mar 05 12:11:54 1999 +0100
+++ b/src/HOL/List.ML	Mon Mar 08 13:49:14 1999 +0100
@@ -837,9 +837,21 @@
 by Auto_tac;
 qed_spec_mp"set_take_whileD";
 
-qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
-qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" 
-						      (K [Simp_tac 1]);
+(** zip **)
+section "zip";
+
+Goal "zip [] ys = []";
+by(induct_tac "ys" 1);
+by Auto_tac;
+qed "zip_Nil";
+Addsimps [zip_Nil];
+
+Goal "zip (x#xs) (y#ys) = (x,y)#zip xs ys";
+by(Simp_tac 1);
+qed "zip_Cons_Cons";
+Addsimps [zip_Cons_Cons];
+
+Delsimps(tl (thms"zip.simps"));
 
 
 (** foldl **)
diff -r 4cbdb974220c -r 81e7fbf61db2 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Mar 05 12:11:54 1999 +0100
+++ b/src/HOL/List.thy	Mon Mar 08 13:49:14 1999 +0100
@@ -140,7 +140,7 @@
   "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
 primrec
   "zip xs []     = []"
-  "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
+  "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
 primrec
   "[i..0(] = []"
   "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"