equal
deleted
inserted
replaced
26 thm trm_assg.distinct |
26 thm trm_assg.distinct |
27 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
27 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
28 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
28 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
29 |
29 |
30 declare permute_trm_raw_permute_assg_raw.simps[eqvt] |
30 declare permute_trm_raw_permute_assg_raw.simps[eqvt] |
31 declare alpha_gen_eqvt[eqvt] |
|
32 |
31 |
33 equivariance alpha_trm_raw |
32 equivariance alpha_trm_raw |
34 |
33 |
35 |
34 |
36 end |
35 end |