src/ZF/thy_syntax.ML
changeset 4502 337c073de95e
parent 3925 90f499226ab9
child 6053 8a1059aa01f0
equal deleted inserted replaced
4501:5f629ee2502b 4502:337c073de95e