src/Pure/General/latex.ML
changeset 80286 00d68f324056
parent 79503 c67b47cd41dc
child 80789 bcecb69f72fa