src/Pure/General/latex.ML
changeset 80225 d9ff4296e3b7
parent 79503 c67b47cd41dc
child 80789 bcecb69f72fa