equal
deleted
inserted
replaced
27 Smaller things: |
27 Smaller things: |
28 |
28 |
29 - maybe <t1_t2>.perm_simps should be called permute_<type>.simps; |
29 - maybe <t1_t2>.perm_simps should be called permute_<type>.simps; |
30 that would conform with the terminology in Nominal2 |
30 that would conform with the terminology in Nominal2 |
31 |
31 |
|
32 - nominal_induct does not work without an induction rule |
|
33 |
|
34 - nominal_induct throws strange "THM" exceptions if not enough |
|
35 variables are given |
|
36 |
|
37 - nominal_induct cannot avoid a term (for example function applied |
|
38 to an argument). |
32 |
39 |
33 Other: |
40 Other: |
34 |
41 |
35 - nested recursion, like types "trm list" in a constructor |
42 - nested recursion, like types "trm list" in a constructor |
36 |
43 |