src/Pure/Syntax/mixfix.ML
changeset 4962 e9217cb15b42
parent 4920 9c4ff93762a0
child 5056 e88cc76cb052