src/Pure/Thy/latex.ML
changeset 75792 4e273b4e04e8
parent 74884 229d7ea628c2
child 76371 1ac2416e8432