src/ZF/thy_syntax.ML
changeset 13368 8f8ba32d148b
parent 12183 c10cea75dd56
child 14598 7009f59711e3