| changeset 2120 | 2786ff1df475 |
| parent 2105 | e25b0fff0dd2 |
| child 2179 | 7687f97eca53 |
| 2119:238062c4c9f2 | 2120:2786ff1df475 |
|---|---|
12 and tys = |
12 and tys = |
13 All xs::"name fset" ty::"ty" bind_res xs in ty |
13 All xs::"name fset" ty::"ty" bind_res xs in ty |
14 |
14 |
15 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] |
15 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] |
16 |
16 |
17 equivariance alpha_ty_raw |
|
18 |
17 |
19 |
18 |
20 (* below we define manually the function for size *) |
19 (* below we define manually the function for size *) |
21 |
20 |
22 lemma size_eqvt_raw: |
21 lemma size_eqvt_raw: |