src/Pure/Thy/thy_header.ML
changeset 39811 0659e84bdc5f
parent 38149 3c380380beac
child 40523 1050315f6ee2