src/Pure/General/latex.scala
changeset 80161 fd5ed5e63a29
parent 79503 c67b47cd41dc
child 80441 c420429fdf4c
equal deleted inserted replaced
80160:ead20482da9c 80161:fd5ed5e63a29