src/Pure/Syntax/mixfix.ML
changeset 18522 9bdfb6eaf8ab
parent 18341 d99396e96632
child 18565 818a24371de9
equal deleted inserted replaced
18521:ee14a65fe764 18522:9bdfb6eaf8ab