src/Pure/General/pretty.scala
changeset 37121 8e51fc35d59f
parent 36820 0cdfce0bf956
child 37374 d66e6cc47fab
equal deleted inserted replaced
37120:5df087c6ce94 37121:8e51fc35d59f