# HG changeset patch
# User nipkow
# Date 1505241646 -7200
# Node ID e9be3d6995f9795e316fa5fe4aabf036f5e42948
# Parent  4a812abde31406553f22c972e3198d6657bf1da9
introduced zip_with

diff -r 4a812abde314 -r e9be3d6995f9 src/HOL/Library/Stirling.thy
--- a/src/HOL/Library/Stirling.thy	Tue Sep 12 12:14:38 2017 +0200
+++ b/src/HOL/Library/Stirling.thy	Tue Sep 12 20:40:46 2017 +0200
@@ -246,7 +246,7 @@
 \<close>
 
 definition zip_with_prev :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'b list"
-  where "zip_with_prev f x xs = map (\<lambda>(x,y). f x y) (zip (x # xs) xs)"
+  where "zip_with_prev f x xs = zip_with f (x # xs) xs"
 
 lemma zip_with_prev_altdef:
   "zip_with_prev f x xs =
diff -r 4a812abde314 -r e9be3d6995f9 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 12 12:14:38 2017 +0200
+++ b/src/HOL/List.thy	Tue Sep 12 20:40:46 2017 +0200
@@ -151,6 +151,9 @@
   \<comment> \<open>Warning: simpset does not contain this definition, but separate
        theorems for \<open>xs = []\<close> and \<open>xs = z # zs\<close>\<close>
 
+abbreviation zip_with :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
+"zip_with f xs ys \<equiv> map (\<lambda>(x,y). f x y) (zip xs ys)"
+
 primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
 "product [] _ = []" |
 "product (x#xs) ys = map (Pair x) ys @ product xs ys"