[isabelle-dev] NEWS: Document preparation engine updates

Makarius makarius at sketis.net
Mon Sep 28 13:01:34 CEST 2020

On 27/09/2020 21:26, Makarius wrote:
> This refers to Isabelle/684f14b1e7fc (and AFP/35158287da0b).
> At the Isabelle Workshop 2020, Clemens Ballarin proposed to switch to LuaLaTeX
> by default: it allows advanced packages programmed in the Lua scripting language.

One more thing: using visual diffpdf on Ubuntu 18.04, I have compared various
important "doc" entries, e.g. prog-prove, jedit, implementation, isar-ref.

After Isabelle/8162ca81ea8a the results are mostly identical, with a few minor
deviations in font-metrics and hyphenation: both work generally better in

There might be more fine points to watch out for.

As a general principle, documents that use Isabelle mechanisms like the
@{verbatim} or @{text} antiquotations work better than low-level
"LaTeX-drawings" done manually (e.g. \verbatim and $...$).


More information about the isabelle-dev mailing list