src/Pure/Thy/thy_element.scala
changeset 78571 ed07f0ebf31c
parent 75405 b13ab7d11b90
child 78912 ff4496b25197