| changeset 2067 | ace7775cbd04 |
| parent 2056 | a58c73e39479 |
| child 2082 | 0854af516f14 |
| 2066:deb732753522 | 2067:ace7775cbd04 |
|---|---|
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] |
|
33 declare alpha_gen_eqvt[eqvt] |
|
34 equivariance alpha_lam_raw |
|
35 *) |
|
36 |
|
32 end |
37 end |
33 |
38 |
34 |
39 |
35 |
40 |