src/Pure/General/symbol.ML
changeset 13049 ce180e5b7fa0
parent 12904 c208d71702d1
child 13559 51c3ac47d127