src/Pure/Thy/thy_parse.ML
changeset 1444 23ceb1dc9755
parent 1383 be42217b0b5c
child 1512 ce37c64244c0