src/Pure/Thy/thy_header.ML
changeset 46811 03a2dc9e0624
parent 46737 09ab89658a5d
child 46938 cda018294515