src/Pure/Syntax/mixfix.ML
changeset 22421 51a18dd1ea86
parent 21805 6af1aa7f67d6
child 22702 372da033ed93
equal deleted inserted replaced
22420:4ccc8c1b08a3 22421:51a18dd1ea86