src/Pure/Syntax/mixfix.ML
changeset 18679 cf9f1584431a
parent 18673 fad60fe1565c
child 18719 dca3ae4f6dd6