--- 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 **)
--- 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 [])"