src/Pure/Syntax/mixfix.ML
changeset 7025 afbd8241797b
parent 6929 16ee7b14a2c1
child 7471 38823cea751f