src/Pure/Syntax/syntax.ML
changeset 569 4dc184a3d09b
parent 556 3f5f42467717
child 624 33b9b5da3e6f