src/Pure/Thy/thy_header.ML
changeset 59173 cdcbda56b05b
parent 58999 ed09ae4ea2d8
child 59693 d96cb03caf9e
equal deleted inserted replaced
59172:d1c500e0a722 59173:cdcbda56b05b