src/ZF/thy_syntax.ML
changeset 8134 ceedd1a8bad6
parent 8127 68c6159440f1
child 8813 abc0f3722aed
equal deleted inserted replaced
8133:ba1498046ee6 8134:ceedd1a8bad6