src/Pure/Thy/latex.ML
changeset 15821 ac7ea72c463b
parent 15801 d2f5ca3c048d
child 17081 e19963723262
equal deleted inserted replaced
15820:63914dbc4645 15821:ac7ea72c463b