src/ZF/thy_syntax.ML
changeset 4707 abe6f28a38c1
parent 3925 90f499226ab9
child 6053 8a1059aa01f0