src/ZF/thy_syntax.ML
changeset 13209 e62a6bd3f085
parent 12183 c10cea75dd56
child 14598 7009f59711e3