Stream: General

Topic: Document generation fails if \<Zprime> is used in theory

view this post on Zulip Poscat (Oct 16 2026 at 05:34):

Repo here: https://github.com/poscat0x04/isabelle-prime-repro
Run isabelle build -D . at project root to reproduce error.
Root cause seems to be that \isasymZprime is undefined in isabellesym.sty

Found a workaround: add

\newcommand{\isasymZprime}{\isamath{^\prime}}

to your root.tex

view this post on Zulip Kevin Kappelmann (Oct 16 2026 at 09:44):

Seems like something that should be sent to the Isabelle developers. Include the Isabelle version you used in your email.

Last updated: Oct 25 2026 at 22:21 UTC