src/Pure/Thy/latex.ML
changeset 73826 72900f34dbb3
parent 73780 466fae6bf22e
child 74779 5fca489a6ac1