[isabelle-dev] Latex problem on the AFP

[Makarius]

On 01/09/2023 10:26, Anders Schlichtkrull wrote:
> 
> My conclusion is that the problem is essentially that in Paraconsistency.thy we have the following:
> 
> text
> ‹
> Theorem valid_in_valid is a kind of the reverse of valid_valid_in (or its transfer variant).
> ›
> 
> In the generated LaTeX this becomes
>    Theorem valid_in_valid is a kind of the reverse of valid_valid_in (or its transfer variant).
> 
> The underscore is a reserved character in LaTeX, and cannot be used in textmode.
> However, we "solved" that "problem" by importing the underscore package.
> That package's documentation states: "A simple “_” acts just like “\_” in text mode"

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.


	Makarius