Email Gateway (Aug 22 2022 at 18:46): Email Gateway (Aug 22 2022 at 18:46):From: Peter Lammich <lammich@in.tum.de>
Hi,
I just learned that \cancel inside a text block will produce LaTex
output that displays the text striked out.
However, is there a way to exclude some content alltogether from the
LaTex output ... a very desireable feature when prototyping papers,
slides, etc. in Isabelle.
Note that LaTeX's % or begin{comment} do not prevent Isabelle from
processing antiquotations, which may fail, or even interfere, in
particular with the end-of-line comment %.
Email Gateway (Aug 22 2022 at 18:46):From: Makarius <makarius@sketis.net>
You can put everything into a default cartouche (antiquotation with the
name "cartouche"). Thus the body is typeset like formal text, e.g. term
language. Putting a Latex comment before it should be able to suppress
the output.
E.g. like this:
%‹foo bar \rubbish @{junk›
Makarius
Last updated: Apr 30 2024 at 08:19 UTC