| changeset 1516 | e3a82a3529ce |
| parent 1510 | be911e869fde |
| child 1527 | e1c74b864b1b |
| 1515:76fa21f27f22 | 1516:e3a82a3529ce |
|---|---|
1 Smaller things: |
1 Smaller things: |
2 |
|
3 - case names for "weak" induction rules (names of the |
|
4 constructors); see page 61/62 and 170 in Tutorial |
|
5 |
2 |
6 - maybe <type>_perm whould be called permute_<type>.simps; |
3 - maybe <type>_perm whould be called permute_<type>.simps; |
7 that would conform with the terminology in Nominal2 |
4 that would conform with the terminology in Nominal2 |
8 |
5 |
9 |
6 |