src/Pure/Syntax/mixfix.ML
changeset 4011 c161162bc8c5
parent 3829 d7333ef9e72c
child 4053 c88d0d5ae806
equal deleted inserted replaced
4010:59cac65fb751 4011:c161162bc8c5