src/Pure/General/symbol.ML
changeset 37724 6607ccf77946
parent 37534 62eb9d03b221
child 37728 5d2b3e827371