equal
deleted
inserted
replaced
10 |
10 |
11 theory Stream |
11 theory Stream |
12 imports "../BNF" |
12 imports "../BNF" |
13 begin |
13 begin |
14 |
14 |
15 codata (sset: 'a) stream (map: smap rel: stream_all2) = |
15 codatatype (sset: 'a) stream (map: smap rel: stream_all2) = |
16 Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) |
16 Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) |
17 |
17 |
18 declaration {* |
18 declaration {* |
19 Nitpick_HOL.register_codatatype |
19 Nitpick_HOL.register_codatatype |
20 @{typ "'stream_element_type stream"} @{const_name stream_case} [dest_Const @{term Stream}] |
20 @{typ "'stream_element_type stream"} @{const_name stream_case} [dest_Const @{term Stream}] |
21 (*FIXME: long type variable name required to reduce the probability of |
21 (*FIXME: long type variable name required to reduce the probability of |