| changeset 2105 | e25b0fff0dd2 |
| parent 2104 | 2205b572bc9b |
| child 2120 | 2786ff1df475 |
| 2104:2205b572bc9b | 2105:e25b0fff0dd2 |
|---|---|
28 thm lam_bp.distinct |
28 thm lam_bp.distinct |
29 thm lam_bp.supp |
29 thm lam_bp.supp |
30 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
30 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
31 thm lam_bp.fv[simplified lam_bp.supp(1-2)] |
31 thm lam_bp.fv[simplified lam_bp.supp(1-2)] |
32 |
32 |
33 declare permute_lam_raw_permute_bp_raw.simps[eqvt] |
|
34 |
|
35 equivariance alpha_lam_raw |
33 equivariance alpha_lam_raw |
36 |
34 |
37 |
35 |
38 end |
36 end |
39 |
37 |