Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Using LaTeX output print mode for source text


view this post on Zulip 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

view this post on Zulip 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: Jul 15 2022 at 23:21 UTC