| changeset 62093 | bd73a2279fcd |
| parent 61681 | ca53150406c9 |
| child 63192 | a742d309afa2 |
| 62092:9ace5f5bae69 | 62093:bd73a2279fcd |
|---|---|
67 |
67 |
68 |
68 |
69 subsection \<open>set of streams with elements in some fixed set\<close> |
69 subsection \<open>set of streams with elements in some fixed set\<close> |
70 |
70 |
71 context |
71 context |
72 notes [[inductive_defs]] |
72 notes [[inductive_internals]] |
73 begin |
73 begin |
74 |
74 |
75 coinductive_set |
75 coinductive_set |
76 streams :: "'a set \<Rightarrow> 'a stream set" |
76 streams :: "'a set \<Rightarrow> 'a stream set" |
77 for A :: "'a set" |
77 for A :: "'a set" |