| changeset 2146 | a2f70c09e77d |
| parent 2120 | 2786ff1df475 |
| child 2200 | 31f1ec832d39 |
| child 2288 | 3b83960f9544 |
| 2145:f89773ab0685 | 2146:a2f70c09e77d |
|---|---|
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 |
31 |
32 |
32 |
33 |
|
33 end |
34 end |
34 |
35 |
35 |
36 |
36 |
37 |