src/Pure/Thy/latex.ML
changeset 73060 4b620e1cb1e9
parent 72315 8162ca81ea8a
child 73754 cd7eb3cdab4c
equal deleted inserted replaced
73059:523806d71dea 73060:4b620e1cb1e9