src/Pure/Thy/thy_parse.ML
changeset 9707 067c25edd1bd
parent 9328 1a46c94d1425
child 11819 9283b3c11234