src/Pure/Thy/latex.ML
changeset 25019 3b2d3b8fc7b6
parent 23703 1b6a2c119151
child 27344 d44490b06190