equal
deleted
inserted
replaced
25 thm trm_assg.inducts |
25 thm trm_assg.inducts |
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] |
|
31 |
|
32 equivariance alpha_trm_raw |
30 equivariance alpha_trm_raw |
33 |
31 |
34 |
32 |
35 end |
33 end |
36 |
34 |