src/Pure/Syntax/symbol.ML
changeset 5526 e7617b57a3e6
parent 5229 7c8abffc4413
child 5870 5d4fc952be47