Email Gateway (Sep 30 2022 at 09:23): Email Gateway (Sep 30 2022 at 09:23):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
There appears to be a LaTeX issue with \isasymlonglonglongrightarrow.
Trying to build a session where the Isabelle symbol
\longlonglongrightarrow is used in a session theory file causes a LaTeX
build failure with an undefined control sequence error:
Undefined control sequence.
\isasymlonglonglongrightarrow ...nglongrightarrow
...artoucheopen}{\isasymlonglonglongrightarrow
Note that this is with amsmath imported as a dependency in the session
root.tex file. Strangely, this error does not occur with
\longlongrightarrow and \isasymlonglongrightarrow despite the two LaTeX
macros being defined next to each other in isabellesym.sty and defined
largely in the same way.
Has anybody seen this issue before?
Thanks,
Dominic
Email Gateway (Oct 06 2022 at 09:54):From: Makarius <makarius@sketis.net>
I have not seen anything like this recently, although LaTeX problems do occur
routinely at times: there are too many different LaTeX distributions around.
There can be also problems in your own Isabelle document setup.
The longlong... arrows are properly rendered e.g. in the "isar-ref" manual
(Appendix B) from Isabelle2022-RC3, see
https://isabelle.sketis.net/website-Isabelle2022-RC3/dist/Isabelle2022-RC3/doc/isar-ref.pdf
The sources for that are here:
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2022-RC3/src/Doc
Makarius
Last updated: Jan 04 2025 at 20:18 UTC