src/ZF/thy_syntax.ML
changeset 13677 5fad004bd9df
parent 12183 c10cea75dd56
child 14598 7009f59711e3