src/Pure/General/symbol.ML
changeset 13025 433c57d09d53
parent 12904 c208d71702d1
child 13559 51c3ac47d127