| changeset 37110 | 7ffdbc24b27f |
| parent 36452 | d37c6eed8117 |
| child 39159 | 0dec18004e75 |
| 37109:e67760c1b851 | 37110:7ffdbc24b27f |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 header {* FOCUS flat streams *} |
9 header {* FOCUS flat streams *} |
10 |
10 |
11 theory Fstream |
11 theory Fstream |
12 imports "../ex/Stream" |
12 imports Stream |
13 begin |
13 begin |
14 |
14 |
15 default_sort type |
15 default_sort type |
16 |
16 |
17 types 'a fstream = "'a lift stream" |
17 types 'a fstream = "'a lift stream" |