equal
deleted
inserted
replaced
27 thm lam_bp.distinct |
27 thm lam_bp.distinct |
28 thm lam_bp.supp |
28 thm lam_bp.supp |
29 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
29 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
30 thm lam_bp.fv[simplified lam_bp.supp(1-2)] |
30 thm lam_bp.fv[simplified lam_bp.supp(1-2)] |
31 |
31 |
32 (*declare permute_lam_raw_permute_bp_raw.simps[eqvt] |
32 declare permute_lam_raw_permute_bp_raw.simps[eqvt] |
33 declare alpha_gen_eqvt[eqvt] |
33 declare alpha_gen_eqvt[eqvt] |
|
34 |
34 equivariance alpha_lam_raw |
35 equivariance alpha_lam_raw |
35 *) |
36 |
36 |
37 |
37 end |
38 end |
38 |
39 |
39 |
40 |
40 |
41 |