src/Pure/Thy/thy_header.ML
changeset 49078 398e8fddabb0
parent 48992 0518bf89c777
child 50128 599c935aac82