src/Pure/Thy/thy_syntax.ML
changeset 40003 427106657e04
parent 39507 839873937ddd
child 40131 7cbebd636e79