Re: [isabelle] Applicability of LaTeXsugar and OptionalSugar

Le Thu, 09 Aug 2012 08:35:11 +0200, Tobias Nipkow <nipkow at> a écrit:

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.


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).

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.