src/Pure/Thy/thy_header.ML
changeset 59117 caddfa6ca534
parent 58999 ed09ae4ea2d8
child 59693 d96cb03caf9e
equal deleted inserted replaced
59116:77351f2051f5 59117:caddfa6ca534