src/Pure/Thy/thy_header.ML
changeset 23513 2ebb50c0db4f
parent 22106 0886ec05f951
child 23677 1114cc909800