equal
deleted
inserted
replaced
19 |
19 |
20 datatype_new (discs_sels) simple'' = X1'' nat int | X2'' |
20 datatype_new (discs_sels) simple'' = X1'' nat int | X2'' |
21 |
21 |
22 datatype_new (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist") |
22 datatype_new (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist") |
23 |
23 |
24 datatype_new (discs_sels) ('b, 'c, 'd, 'e) some_passive = |
24 datatype_new (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive = |
25 SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e |
25 SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e |
26 |
26 |
27 datatype_new (discs_sels) hfset = HFset "hfset fset" |
27 datatype_new (discs_sels) hfset = HFset "hfset fset" |
28 |
28 |
29 datatype_new (discs_sels) lambda = |
29 datatype_new (discs_sels) lambda = |