src/Pure/Thy/latex.ML
changeset 9721 7e51c9f3d5a0
parent 9707 067c25edd1bd
child 9749 36ddd544a18d