| changeset 62093 | bd73a2279fcd |
| parent 61681 | ca53150406c9 |
| child 63192 | a742d309afa2 |
--- a/src/HOL/Library/Stream.thy Thu Jan 07 15:50:09 2016 +0100 +++ b/src/HOL/Library/Stream.thy Thu Jan 07 15:53:39 2016 +0100 @@ -69,7 +69,7 @@ subsection \<open>set of streams with elements in some fixed set\<close> context - notes [[inductive_defs]] + notes [[inductive_internals]] begin coinductive_set