Email Gateway (Dec 09 2020 at 16:36): Email Gateway (Dec 09 2020 at 16:36):From: Manuel Eberl <eberlm@in.tum.de>
Is there any way to force Isabelle to print source text (definitions,
theorem statements, proofs, etc.) to LaTeX not the way it was typed, but
with abbreviations?
I.e. if I define an abbreviation "|X| = card X" and I have
lemma "card X = 1"
I want the LaTeX output to show "|X|", not "card X".
Manuel
smime.p7s
Email Gateway (Jan 02 2021 at 10:48):From: Makarius <makarius@sketis.net>
In general, applying force is not going to work in the long run, and often
causes a lot of harm.
Isabelle2021 will have much more formal document markup in standard builds,
allowing better HTML presentation, for example.
At a later stage that might impact PDF document preparation as well, but it
might require a long time to get there.
Term abbreviations or notations are more difficult, and not part of existing
concepts so far.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC