src/Pure/Syntax/mixfix.ML
changeset 21966 edab0ecfbd7c
parent 21805 6af1aa7f67d6
child 22702 372da033ed93