src/Pure/Syntax/mixfix.ML
changeset 41985 09b75d55008f
parent 37216 3165bc303f66
child 42130 e10e2cce85c8
equal deleted inserted replaced
41984:e5dba3d75e9e 41985:09b75d55008f