src/Pure/Thy/thy_parse.ML
changeset 10579 1db42f739ee7
parent 9328 1a46c94d1425
child 11819 9283b3c11234
equal deleted inserted replaced
10578:b32513971481 10579:1db42f739ee7