src/Pure/Thy/thy_element.scala
changeset 78730 a9ac75d397df
parent 75405 b13ab7d11b90
child 78912 ff4496b25197