| changeset 58310 | 91ea607a34d8 |
| parent 58249 | 180f1b3508ed |
| child 58889 | 5b7a9633cfa8 |
| 58309:a09ec6daaa19 | 58310:91ea607a34d8 |
|---|---|
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_new ('a, 'b) foo = |
45 datatype ('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 |