src/HOL/List.thy

--- a/src/HOL/List.thy	Sat Apr 17 23:05:52 2010 +0200
+++ b/src/HOL/List.thy	Mon Apr 19 07:38:35 2010 +0200
@@ -1943,6 +1943,12 @@
 
 declare zip_Cons [simp del]
 
+lemma [code]:
+  "zip [] ys = []"
+  "zip xs [] = []"
+  "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
+  by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
+
 lemma zip_Cons1:
  "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
 by(auto split:list.split)