src/Pure/Syntax/mixfix.ML
changeset 19346 c4c003abd830
parent 19271 967e6c2578f2
child 19373 f2446ce04590