[isabelle-dev] Latex problem on the AFP

[Anders Schlichtkrull]

> 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.

  Anders