src/Pure/Syntax/mixfix.ML
changeset 17120 4ddeef83bd66
parent 16610 58bf09036a6d
child 17284 ca3eebbb3724
equal deleted inserted replaced
17119:b241ba3eb4db 17120:4ddeef83bd66