changeset 66655 | e9be3d6995f9 |
parent 65552 | f533820e7248 |
child 66656 | 8f4d252ce2fe |
--- 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 =