src/Pure/General/symbol.scala
changeset 44262 355d5438f5fb
parent 44238 36120feb70ed
child 44949 b49d7f1066c8