src/Pure/Thy/latex.ML
changeset 77325 5158dc9d096b
parent 76957 deb7dffb3340
child 77768 65008644d394
equal deleted inserted replaced
77321:cf6947717650 77325:5158dc9d096b