Email Gateway (Aug 22 2022 at 15:16): Email Gateway (Aug 22 2022 at 15:16):From: Slawomir Kolodynski via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
In my attempt to update IsarMathLib to Isabelle2016-1 I got the following error when processing the IsarMathLib session from command line:
*** l.155 \input{Metamath_
*** Sampler.tex}
*** ! Extra }, or forgotten $.
*** l.155 \input{Metamath_Sampler.tex}
The line number is in Isabelle generated session.tex file so LateX seems to complain about the underscore in a theory name. I can see that theory names with underscores are still supported, so what I should do here to fix this error?
Kind regards
Slawomir Kolodynski http://savannah.nongnu.org/projects/isarmathlib Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Email Gateway (Aug 22 2022 at 15:16):From: Makarius <makarius@sketis.net>
I am not aware of any change on the Isabelle side. Underscores are the
standard way to separate words in identifiers of all kinds
(CamelCaseIsNotUsedInOrderToImproveReadability).
I guess that you have changed something in the LaTeX style setup on your
side, or it is a different LaTeX installation.
Makarius
Last updated: Apr 19 2024 at 04:17 UTC