--- a/src/HOL/Library/Stream.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Library/Stream.thy Sun Nov 15 12:39:51 2015 +0100
@@ -68,12 +68,18 @@
subsection \<open>set of streams with elements in some fixed set\<close>
+context
+ notes [[inductive_defs]]
+begin
+
coinductive_set
streams :: "'a set \<Rightarrow> 'a stream set"
for A :: "'a set"
where
Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
+end
+
lemma in_streams: "stl s \<in> streams S \<Longrightarrow> shd s \<in> S \<Longrightarrow> s \<in> streams S"
by (cases s) auto