[isabelle-dev] Latex problem on the AFP

Lawrence Paulson lp15 at cam.ac.uk
Fri Sep 1 11:48:27 CEST 2023

Please don’t do this! Don’t be afraid to type \_ if you have to.

On 1 Sep 2023 at 09:27 +0100, Anders Schlichtkrull <andsch at cs.aau.dk>, wrote:

However, we "solved" that "problem" by importing the underscore package.
That package's documentation states: "A simple “_” acts just like “\_” in text mode"
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230901/669b8624/attachment.htm>

More information about the isabelle-dev mailing list