src/Pure/Thy/latex.ML
changeset 73718 ecb31c3bf980
parent 72315 8162ca81ea8a
child 73754 cd7eb3cdab4c
equal deleted inserted replaced
73717:2f4cb9cb087f 73718:ecb31c3bf980