| branch | Nominal2-Isabelle2013 |
| changeset 3208 | da575186d492 |
| parent 3065 | 51ef8a3cb6ef |
| 3206:fb201e383f1b | 3208:da575186d492 |
|---|---|
6 (* |
6 (* |
7 plain nominal_datatype definition without an |
7 plain nominal_datatype definition without an |
8 atom_decl - example by John Matthews |
8 atom_decl - example by John Matthews |
9 *) |
9 *) |
10 |
10 |
11 nominal_datatype 'a::fs Maybe = |
11 |
12 nominal_datatype 'a Maybe = |
|
12 Nothing |
13 Nothing |
13 | Just 'a |
14 | Just 'a |
14 |
15 |
15 |
16 |
16 thm Maybe.distinct |
17 thm Maybe.distinct |