Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Stream.thy
changeset 61424 c3658c18b7bc
parent 60500 903bb1495239
child 61681 ca53150406c9 
--- a/src/HOL/Library/Stream.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/Stream.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -581,7 +581,7 @@
   by (subst smap2.ctr) simp
 
 lemma smap2_szip:
-  "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
+  "smap2 f s1 s2 = smap (case_prod f) (szip s1 s2)"
   by (coinduction arbitrary: s1 s2) auto
 
 lemma smap_smap2[simp]:
@@ -597,7 +597,7 @@
   by (induct n arbitrary: s1 s2) auto
 
 lemma stake_smap2[simp]:
-  "stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))"
+  "stake n (smap2 f s1 s2) = map (case_prod f) (zip (stake n s1) (stake n s2))"
   by (induct n arbitrary: s1 s2) auto
 
 lemma sdrop_smap2[simp]:
isabelle