src/Pure/Syntax/mixfix.ML
changeset 5691 3a6de95c09d0
parent 5690 4b056ee5435c
child 6027 9dd06eeda95c