src/Pure/Thy/latex.ML
changeset 72847 9dda93a753b1
parent 72315 8162ca81ea8a
child 73754 cd7eb3cdab4c