equal
deleted
inserted
replaced
11 | Fun "ty" "ty" |
11 | Fun "ty" "ty" |
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 |
|
17 declare permute_ty_raw_permute_tys_raw.simps[eqvt] |
|
18 declare alpha_gen_eqvt[eqvt] |
|
19 equivariance alpha_ty_raw |
|
20 |
16 |
21 |
17 (* below we define manually the function for size *) |
22 (* below we define manually the function for size *) |
18 |
23 |
19 lemma size_eqvt_raw: |
24 lemma size_eqvt_raw: |
20 "size (pi \<bullet> t :: ty_raw) = size t" |
25 "size (pi \<bullet> t :: ty_raw) = size t" |