src/Pure/General/symbol.ML
changeset 13145 59bc43b51aa2
parent 12904 c208d71702d1
child 13559 51c3ac47d127