src/ZF/thy_syntax.ML
changeset 14722 8e739a6eaf11
parent 14598 7009f59711e3
child 15570 8d8c70b41bab