src/ZF/thy_syntax.ML
changeset 14060 c0c4af41fa3b
parent 12183 c10cea75dd56
child 14598 7009f59711e3