src/Pure/Syntax/mixfix.ML
changeset 5691 3a6de95c09d0
parent 5690 4b056ee5435c
child 6027 9dd06eeda95c
equal deleted inserted replaced
5690:4b056ee5435c 5691:3a6de95c09d0