src/Pure/General/symbol.scala
changeset 32720 fc32e6771749
parent 31929 ecfc667cac53
child 33998 fc56cfc6906e