src/Pure/Syntax/symbol.ML
changeset 4962 e9217cb15b42
parent 4959 4ebdea556457
child 5112 9e74cf11e4a4