src/Pure/Thy/thy_parse.ML
changeset 1444 23ceb1dc9755
parent 1383 be42217b0b5c
child 1512 ce37c64244c0
equal deleted inserted replaced
1443:ff8a804e0201 1444:23ceb1dc9755