| changeset 2120 | 2786ff1df475 |
| parent 2118 | 0e52851acac4 |
| child 2146 | a2f70c09e77d |
| 2119:238062c4c9f2 | 2120:2786ff1df475 |
|---|---|
26 thm trm_assg.inducts |
26 thm trm_assg.inducts |
27 thm trm_assg.distinct |
27 thm trm_assg.distinct |
28 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
28 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
29 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
29 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
30 |
30 |
31 equivariance alpha_trm_raw |
|
32 |
31 |
33 |
32 |
34 end |
33 end |
35 |
34 |
36 |
35 |