[isabelle-dev] NEWS: Improved LaTeX typesetting of ‹...›

Makarius makarius at sketis.net
Thu Mar 11 11:30:33 CET 2021

*** Document preparation ***

* Improved LaTeX typesetting of ‹...› using \guilsinglleft ...
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
(which is now also the default in "isabelle mkroot").

This refers to Isabelle/fbd69f277699, but the actual change is in

I also wanted to upgrade «...» to use \guillemotleft ... \guillemotright from
\usepackage[T1]{fontenc}, but this did not work, because the LaTeX/Linux
installation of various test machines at TUM is very old (Ubuntu 16.04).

Why are we still testing ancient LaTeX? With LuaLaTeX we are now at the
frontier of ongoing LaTeX development. Many old problems go away if recent
installation is used.


More information about the isabelle-dev mailing list