src/Pure/Syntax/mixfix.ML
changeset 18522 9bdfb6eaf8ab
parent 18341 d99396e96632
child 18565 818a24371de9