src/Pure/Thy/latex.ML
changeset 38266 492d377ecfe2
parent 37533 d775bd70f571
child 39479 465064e8f269