| changeset 2200 | 31f1ec832d39 |
| parent 2146 | a2f70c09e77d |
| child 2213 | 231a20534950 |
| child 2303 | c785fff02a8f |
| 2195:0c1dcdefb515 | 2200:31f1ec832d39 |
|---|---|
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 |
31 |
32 |
|
33 |
|
34 end |
32 end |
35 |
33 |
36 |
34 |
37 |
35 |