src/Pure/Thy/thy_header.ML
changeset 23719 ccd9cb15c062
parent 23677 1114cc909800
child 23863 8f3099589cfa