# HG changeset patch
# User traytel
# Date 1362500282 -3600
# Node ID ae707530c35955d698c5d8164f572a1f8db40dd9
# Parent  fdecc2cd56493b9a0e485cf50553f28c7490f361
extended stream library a little more

diff -r fdecc2cd5649 -r ae707530c359 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Tue Mar 05 17:10:49 2013 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy	Tue Mar 05 17:18:02 2013 +0100
@@ -52,6 +52,9 @@
   "shift [] s = s"
 | "shift (x # xs) s = x ## shift xs s"
 
+lemma stream_map_shift[simp]: "stream_map f (xs @- s) = map f xs @- stream_map f s"
+  by (induct xs) auto
+
 lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
   by (induct xs) auto