equal
deleted
inserted
replaced
1 Smaller things: |
1 Smaller things: |
2 |
2 |
3 - case names for "weak" induction rules (names of the |
3 - case names for "weak" induction rules (names of the |
4 constructors); see page 61/62 and 170 in Tutorial |
4 constructors); see page 61/62 and 170 in Tutorial |
5 |
5 |
6 - <type>_perm rules should be added to the simplifier; |
6 - maybe <type>_perm whould be called permute_<type>.simps; |
7 maybe <type>_perm whould be called permute_<type>.simps; |
|
8 that would conform with the terminology in Nominal2 |
7 that would conform with the terminology in Nominal2 |
9 |
|
10 - <type>_fv / <type>_bn / <type>_distinct should also be |
|
11 added to the simplifier |
|
12 |
8 |
13 |
9 |
14 Bigger things: |
10 Bigger things: |
15 |
11 |
16 - nested recursion, like types "trm list" in a constructor |
12 - nested recursion, like types "trm list" in a constructor |