equal
deleted
inserted
replaced
1 theory Compat |
1 theory Compat |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 |
|
6 datatype_new 'a lst = Nl | Cns 'a "'a lst" |
5 datatype_new 'a lst = Nl | Cns 'a "'a lst" |
7 datatype_compat lst |
6 datatype_compat lst |
8 |
7 |
9 datatype_new 'b w = W | W' "'b w * 'b list" |
8 datatype_new 'b w = W | W' "'b w \<times> 'b list" |
10 (* no support for sums of products |
9 (* no support for sums of products |
11 datatype_compat w |
10 datatype_compat w |
12 *) |
11 *) |
13 |
12 |
14 datatype_new ('c, 'b) s = L 'c | R 'b |
13 datatype_new ('c, 'b) s = L 'c | R 'b |
68 |
67 |
69 datatype funky = Funky "funky tre" | Funky' |
68 datatype funky = Funky "funky tre" | Funky' |
70 datatype fnky = Fnky "nat tre" |
69 datatype fnky = Fnky "nat tre" |
71 |
70 |
72 datatype_new tree = Tree "tree foo" |
71 datatype_new tree = Tree "tree foo" |
73 datatype_compat tree |
72 (* FIXME: datatype_compat tree *) |
74 |
73 |
75 ML {* Datatype_Data.get_info @{theory} @{type_name tree} *} |
74 ML {* Datatype_Data.get_info @{theory} @{type_name tree} *} |
76 |
75 |
77 end |
76 end |