src/Pure/Syntax/mixfix.ML
changeset 569 4dc184a3d09b
parent 551 4c139c37dbaf
child 624 33b9b5da3e6f