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 |
11 nominal_datatype 'a Maybe = |
11 nominal_datatype 'a Maybe = |
12 Nothing |
12 Nothing |
13 | Just 'a |
13 | Just 'a |
14 |
14 |
15 |
15 |
21 thm Maybe.perm_simps |
21 thm Maybe.perm_simps |
22 thm Maybe.eq_iff |
22 thm Maybe.eq_iff |
23 thm Maybe.fv_bn_eqvt |
23 thm Maybe.fv_bn_eqvt |
24 thm Maybe.size_eqvt |
24 thm Maybe.size_eqvt |
25 thm Maybe.supp |
25 thm Maybe.supp |
26 *) |
|
27 |
26 |
28 (* |
27 (* |
29 using a datatype inside a nominal_datatype |
28 using a datatype inside a nominal_datatype |
30 *) |
29 *) |
31 |
30 |