src/Pure/Thy/thy_header.ML
changeset 59066 45ab32a542fe
parent 58999 ed09ae4ea2d8
child 59693 d96cb03caf9e