src/Pure/Thy/latex.ML
changeset 24854 0ebcd575d3c6
parent 23703 1b6a2c119151
child 27344 d44490b06190