src/Pure/Thy/latex.ML
changeset 78018 dfa44d85d751
parent 77851 ec50b9213969