equal
deleted
inserted
replaced
10 instance ty1 and tyn :: fs |
10 instance ty1 and tyn :: fs |
11 ty1_tyn.supp empty when for too many bindings |
11 ty1_tyn.supp empty when for too many bindings |
12 |
12 |
13 Smaller things: |
13 Smaller things: |
14 |
14 |
|
15 - lam.perm should be called permute_lam.simps (that is |
|
16 the convention from Nominal2) |
|
17 |
15 - maybe <type>_perm whould be called permute_<type>.simps; |
18 - maybe <type>_perm whould be called permute_<type>.simps; |
16 that would conform with the terminology in Nominal2 |
19 that would conform with the terminology in Nominal2 |
17 |
20 |
18 - we also need to lift the size function for nominal |
21 - we also need to lift the size function for nominal |
19 datatypes |
22 datatypes |
|
23 |
|
24 - Abs.thy contains lemmas for equivariance of the alphas; |
|
25 they are not yet used anywhere |
20 |
26 |
21 Bigger things: |
27 Bigger things: |
22 |
28 |
23 - the alpha equivalence for |
29 - the alpha equivalence for |
24 |
30 |