Re: [isabelle] Applicability of LaTeXsugar and OptionalSugar

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.


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

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