src/Pure/Syntax/mixfix.ML
changeset 20854 f9cf9e62d11c
parent 20786 96077403f619
child 20892 318f0ff93d99