src/Pure/General/symbol.ML
changeset 20183 fd546b0c8a7c
parent 20067 26bac504ef90
child 20192 956cd30ef3be