src/Pure/Thy/latex.ML
changeset 38422 f96394dba335
parent 37533 d775bd70f571
child 39479 465064e8f269
equal deleted inserted replaced
38421:6cfc6fce7bfb 38422:f96394dba335