src/Pure/Thy/latex.ML
changeset 25456 6f79698f294d
parent 23703 1b6a2c119151
child 27344 d44490b06190