equal
deleted
inserted
replaced
7 ty1_tyn.eq_iff |
7 ty1_tyn.eq_iff |
8 ty1_tyn.induct |
8 ty1_tyn.induct |
9 ty1_tyn.inducts |
9 ty1_tyn.inducts |
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 |
|
13 Parser should check that: |
|
14 - types of bindings match types of binding functions |
|
15 - fsets are not bound in lst bindings |
|
16 - bound arguments are not datatypes |
12 |
17 |
13 Smaller things: |
18 Smaller things: |
14 |
19 |
15 - lam.perm should be called permute_lam.simps (that is |
20 - lam.perm should be called permute_lam.simps (that is |
16 the convention from Nominal2) |
21 the convention from Nominal2) |