src/Pure/Syntax/mixfix.ML
changeset 17658 ab7954ba5261
parent 17284 ca3eebbb3724
child 17787 b6e0d8323c0e