“Device Independent”: format of files produced by TE X