src/Pure/General/symbol.ML
changeset 29055 edaef19665e6
parent 27903 af1b39debf30
child 29324 e07fc65e296b