src/Pure/Thy/latex.ML
changeset 45107 76fef3e57004
parent 43709 717e96cf9527
child 45666 d83797ef0d2d