[isabelle] Applicability of LaTeXsugar and OptionalSugar



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?


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