src/Pure/Syntax/syntax.ML
changeset 609 6d520505e704
parent 556 3f5f42467717
child 624 33b9b5da3e6f