Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Applicability of LaTeXsugar and OptionalSugar

Email Gateway (Aug 19 2022 at 08:13):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
OK. So it's better to expect good presentation from editing and to not
rely too much on sugars. I believe I will even avoid it, as this make
symbols in anti‑quotations and in proofs, different, which I feel is
disturbing, may lead a reader to wonder if it's the same or not. Maybe
using alternative notations for a whole theory is a better option, don't
know, will test it (still on the testing and learning stage).

Email Gateway (Aug 19 2022 at 08:35):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all the people,

As presentation is important, I've played a bit with LaTeXsugar and
OptionalSugar, which together produce nicer output, especially if you use
these with the mathpartir, amsmath and amssymb LaTeX packages.

The sole important thing I could not solve, but may be it's the normal way
of these presentation theories to work, is that it seems to apply on
antiquotations only, not on proofs and definitions text. Ex. the Cons
infix operator, as in “x # xs” is indeed turned into “x · xs” within
anti‑quotations (@{thm …}, @{term …}, and etc) but not in fun, proof, and
al.

Is this a miss‑configuration error of mine or the expected behavior?

Email Gateway (Aug 19 2022 at 08:35):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 09/08/2012 02:11, schrieb Yannick Duchêne (Hibou57):

Hi all the people,

As presentation is important, I've played a bit with LaTeXsugar and
OptionalSugar, which together produce nicer output, especially if you use these
with the mathpartir, amsmath and amssymb LaTeX packages.

The sole important thing I could not solve, but may be it's the normal way of
these presentation theories to work, is that it seems to apply on antiquotations
only, not on proofs and definitions text. Ex. the Cons infix operator, as in “x

xs” is indeed turned into “x · xs” within anti‑quotations (@{thm …}, @{term

…}, and etc) but not in fun, proof, and al.

Correct. This is not a bug but a feature: formal Isabelle text (defs, lemmas,
proofs, ...) is reproduced as it is. This is important because it preserves the
layout. Antiquotations are pretty-printed.

Tobias

Is this a miss‑configuration error of mine or the expected behavior?

Last updated: Nov 21 2024 at 12:39 UTC