equal
deleted
inserted
replaced
|
1 Automatically created functions: |
|
2 |
|
3 ty1_tyn.bn[simp] lifted equations for bn funs |
|
4 ty1_tyn.fv[simp] lifted equations for fv funs |
|
5 ty1_tyn.perm[simp] lifted permutation equations |
|
6 ty1_tyn.distinct[simp] lifted distincts |
|
7 ty1_tyn.eq_iff |
|
8 ty1_tyn.induct |
|
9 ty1_tyn.inducts |
|
10 instance ty1 and tyn :: fs |
|
11 ty1_tyn.supp for too many bindings empty |
|
12 |
1 Smaller things: |
13 Smaller things: |
2 |
14 |
3 - maybe <type>_perm whould be called permute_<type>.simps; |
15 - maybe <type>_perm whould be called permute_<type>.simps; |
4 that would conform with the terminology in Nominal2 |
16 that would conform with the terminology in Nominal2 |
5 |
17 |