src/Pure/Thy/thy_header.ML
changeset 69376 53194e2a969d
parent 69366 b6dacf6eabe3
child 69876 b49bd228ac8a