changeset 41413 | 64cd30d6b0b8 |
parent 40774 | 0437dbc127b3 |
child 51717 | 9e7d1c139569 |
41412:35f30e07fe0d | 41413:64cd30d6b0b8 |
---|---|
97 L1) (? f. is_f f ) --> (? g. def_g g) (trivial) |
97 L1) (? f. is_f f ) --> (? g. def_g g) (trivial) |
98 |
98 |
99 *) |
99 *) |
100 |
100 |
101 theory Focus_ex |
101 theory Focus_ex |
102 imports Stream |
102 imports "~~/src/HOL/HOLCF/Library/Stream" |
103 begin |
103 begin |
104 |
104 |
105 typedecl ('a, 'b) tc |
105 typedecl ('a, 'b) tc |
106 arities tc:: (pcpo, pcpo) pcpo |
106 arities tc:: (pcpo, pcpo) pcpo |
107 |
107 |