diff -r f8fca14c8cbd -r 41ebc19276ea src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Aug 08 12:00:45 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Thu Aug 08 12:01:02 2013 +0200
@@ -239,6 +239,17 @@
   qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
 qed
 
+definition "sfilter P = stream_unfold (shd o sdrop_while (Not o P)) (stl o sdrop_while (Not o P))"
+
+lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
+proof (cases "P x")
+  case True thus ?thesis unfolding sfilter_def
+    by (subst stream.unfold) (simp add: sdrop_while_Stream)
+next
+  case False thus ?thesis unfolding sfilter_def
+    by (subst (1 2) stream.unfold) (simp add: sdrop_while_Stream)
+qed
+
 
 subsection {* unary predicates lifted to streams *}