src/Pure/General/symbol.scala
changeset 77287 d060545f01a2
parent 76235 16c12979c132
child 78592 fdfe9b91d96e