src/Pure/Syntax/mixfix.ML
changeset 4377 2cba48b0f1c4
parent 4143 4bd5f4c05cf6
child 4697 101d384b69b2