[isabelle-dev] Latex problem on the AFP

[Lawrence Paulson]

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

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