src/Pure/System/standard_system.scala
changeset 37724 6607ccf77946
parent 36193 067a01827fca
child 38264 205b74a1bb18
equal deleted inserted replaced
37723:831b3eb7ed8e 37724:6607ccf77946