src/Pure/Thy/thy_parse.ML
changeset 11295 66925f23ac7f
parent 9328 1a46c94d1425
child 11819 9283b3c11234
equal deleted inserted replaced
11294:16481a4cc9f3 11295:66925f23ac7f