src/Pure/Syntax/mixfix.ML
changeset 80967 980cc422526e
parent 80920 bbe2c56fe255
child 81212 b5836dd39018