src/Pure/General/symbol.ML
changeset 25456 6f79698f294d
parent 24593 1547ea587f5a
child 25521 6cebd2ff3ab7