equal
deleted
inserted
replaced
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 declare permute_ty_raw_permute_tys_raw.simps[eqvt] |
|
18 equivariance alpha_ty_raw |
17 equivariance alpha_ty_raw |
19 |
18 |
20 |
19 |
21 (* below we define manually the function for size *) |
20 (* below we define manually the function for size *) |
22 |
21 |