equal
deleted
inserted
replaced
5 (* |
5 (* |
6 plain nominal_datatype definition without an |
6 plain nominal_datatype definition without an |
7 atom_decl - example by John Matthews |
7 atom_decl - example by John Matthews |
8 *) |
8 *) |
9 |
9 |
|
10 (* FIXME: throws an problem with fv-function |
10 nominal_datatype 'a Maybe = |
11 nominal_datatype 'a Maybe = |
11 Nothing |
12 Nothing |
12 | Just 'a |
13 | Just 'a |
13 |
14 |
14 |
15 |
20 thm Maybe.perm_simps |
21 thm Maybe.perm_simps |
21 thm Maybe.eq_iff |
22 thm Maybe.eq_iff |
22 thm Maybe.fv_bn_eqvt |
23 thm Maybe.fv_bn_eqvt |
23 thm Maybe.size_eqvt |
24 thm Maybe.size_eqvt |
24 thm Maybe.supp |
25 thm Maybe.supp |
|
26 *) |
25 |
27 |
26 (* |
28 (* |
27 using a datatype inside a nominal_datatype |
29 using a datatype inside a nominal_datatype |
28 *) |
30 *) |
29 |
31 |