equal
deleted
inserted
replaced
8 |
8 |
9 (* FOCUS flat streams *) |
9 (* FOCUS flat streams *) |
10 |
10 |
11 Fstream = Stream + |
11 Fstream = Stream + |
12 |
12 |
13 default term |
13 default type |
14 |
14 |
15 types 'a fstream = ('a lift) stream |
15 types 'a fstream = ('a lift) stream |
16 |
16 |
17 consts |
17 consts |
18 |
18 |