src/ZF/thy_syntax.ML
changeset 4502 337c073de95e
parent 3925 90f499226ab9
child 6053 8a1059aa01f0