| changeset 58249 | 180f1b3508ed |
| parent 56927 | 4044a7d1720f |
| child 58310 | 91ea607a34d8 |
| 58248:25af24e1f37b | 58249:180f1b3508ed |
|---|---|
40 |
40 |
41 value "[(nat 100, ())]" |
41 value "[(nat 100, ())]" |
42 |
42 |
43 text {* a fancy datatype *} |
43 text {* a fancy datatype *} |
44 |
44 |
45 datatype ('a, 'b) foo = |
45 datatype_new ('a, 'b) foo = |
46 Foo "'a\<Colon>order" 'b |
46 Foo "'a\<Colon>order" 'b |
47 | Bla "('a, 'b) bar" |
47 | Bla "('a, 'b) bar" |
48 | Dummy nat |
48 | Dummy nat |
49 and ('a, 'b) bar = |
49 and ('a, 'b) bar = |
50 Bar 'a 'b |
50 Bar 'a 'b |