src/Pure/Thy/thy_header.ML
changeset 46851 c6235baf20e0
parent 46737 09ab89658a5d
child 46938 cda018294515