# HG changeset patch
# User haftmann
# Date 1271655515 -7200
# Node ID 4d220994f30ba5927dc68598614fb396bf1d66f9
# Parent  2e92aca73cab416a16fe21f68b29465064babcf8# Parent  ead2db2be11a809f809f77f4f5ddf305857d0c9f
merged

diff -r 2e92aca73cab -r 4d220994f30b 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)