src/Pure/Thy/latex.ML
changeset 78254 50a949d316d3
parent 77851 ec50b9213969