src/Pure/Syntax/syntax.ML
changeset 610 ede55dd46f9d
parent 556 3f5f42467717
child 624 33b9b5da3e6f