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