src/HOL/Library/Stirling.thy
changeset 66656 8f4d252ce2fe
parent 66655 e9be3d6995f9
child 68406 6beb45f6cf67
     1.1 --- a/src/HOL/Library/Stirling.thy	Tue Sep 12 20:40:46 2017 +0200
     1.2 +++ b/src/HOL/Library/Stirling.thy	Wed Sep 13 17:40:54 2017 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4  \<close>
     1.5  
     1.6  definition zip_with_prev :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'b list"
     1.7 -  where "zip_with_prev f x xs = zip_with f (x # xs) xs"
     1.8 +  where "zip_with_prev f x xs = map2 f (x # xs) xs"
     1.9  
    1.10  lemma zip_with_prev_altdef:
    1.11    "zip_with_prev f x xs =