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