src/Pure/Thy/thy_parse.ML
changeset 1390 bf523422a3df
parent 1383 be42217b0b5c
child 1512 ce37c64244c0