src/ZF/thy_syntax.ML
changeset 3670 9fea3562f8c7
parent 3622 85898be702b2
child 3925 90f499226ab9