src/Pure/Thy/latex.ML
changeset 37023 efc202e1677e
parent 36959 f5417836dbea
child 37533 d775bd70f571
equal deleted inserted replaced
37022:f9681d9d1d56 37023:efc202e1677e