[isabelle-dev] Latex problem on the AFP

Anders Schlichtkrull andsch at cs.aau.dk
Fri Sep 1 10:53:00 CEST 2023

> On 1 Sep 2023, at 10.36, Makarius <makarius at sketis.net> wrote:
> The underscore package is rubbish.
> When you have formal text inside informal text, the proper way is to use formal markup (via suitable antiquotation). For example:
> text
>> Theorem ‹valid_in_valid› is a kind of the reverse of valid_valid_in (or its transfer variant).
> Here the antiquotation is called "cartouche" and its argument is a single cartouche. Thus the rather short and concise notation with a pair of French single quotes.

OK, I see. Then I will try that instead.


More information about the isabelle-dev mailing list