src/Pure/Thy/latex.ML
changeset 56053 030531cc4c62
parent 55828 42ac3cfb89f6
child 58716 23a380cc45f4