src/Pure/Thy/thy_header.ML
changeset 52808 143f225e50f5
parent 51627 589daaf48dba
child 53962 65bca53daf70