src/Pure/General/symbol.scala
changeset 80539 34a5ca6fcddd
parent 80480 972f7a4cdc0e
child 80548 d1662f1296db