src/Pure/Thy/latex.ML
changeset 9619 6125cc9efc18
parent 9558 8d5221bf765b
child 9663 e4d58f1be05b