src/ZF/thy_syntax.ML
changeset 12175 5cf58a1799a7
parent 12132 1ef58b332ca9
child 12183 c10cea75dd56