src/Pure/Thy/latex.ML
changeset 40442 19faffbe5066
parent 40402 b646316f8b3c
child 40523 1050315f6ee2
equal deleted inserted replaced
40441:0813106a699d 40442:19faffbe5066