src/Pure/Thy/latex.ML
changeset 62631 c39614ddb80b
parent 61595 3591274c607e
child 63590 4854f7ee0987
equal deleted inserted replaced
62630:bc772694cfbd 62631:c39614ddb80b