equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Admissibility for streams *} |
6 header {* Admissibility for streams *} |
7 |
7 |
8 theory Stream_adm |
8 theory Stream_adm |
9 imports Stream Continuity |
9 imports "../ex/Stream" Continuity |
10 begin |
10 begin |
11 |
11 |
12 definition |
12 definition |
13 stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where |
13 stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where |
14 "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow> |
14 "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow> |