src/Pure/Thy/latex.ML
changeset 72638 2a7fc87495e0
parent 72315 8162ca81ea8a
child 73754 cd7eb3cdab4c