src/HOL/Library/Stream.thy
changeset 61424 c3658c18b7bc
parent 60500 903bb1495239
child 61681 ca53150406c9
     1.1 --- a/src/HOL/Library/Stream.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Library/Stream.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -581,7 +581,7 @@
     1.4    by (subst smap2.ctr) simp
     1.5  
     1.6  lemma smap2_szip:
     1.7 -  "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
     1.8 +  "smap2 f s1 s2 = smap (case_prod f) (szip s1 s2)"
     1.9    by (coinduction arbitrary: s1 s2) auto
    1.10  
    1.11  lemma smap_smap2[simp]:
    1.12 @@ -597,7 +597,7 @@
    1.13    by (induct n arbitrary: s1 s2) auto
    1.14  
    1.15  lemma stake_smap2[simp]:
    1.16 -  "stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))"
    1.17 +  "stake n (smap2 f s1 s2) = map (case_prod f) (zip (stake n s1) (stake n s2))"
    1.18    by (induct n arbitrary: s1 s2) auto
    1.19  
    1.20  lemma sdrop_smap2[simp]: