Re: [isabelle] A few questions about LaTeX theory output

The only symbol for the empty set in Isabelle is "{}". Hence you can only obtain the latex \emptyset via antiquotations, not in the sources. However, you can modify Library/LaTeXsugar as follows:


syntax (latex output)
  "_emptyset" :: "'a set"              ("...")
  "_emptyset"      <= "{}"


notation (latex)
  "{}" ("\<emptyset>")

If you import LaTeXsugar into a theory, you may now use \<emptyset> in it.

We may modify LaTeXsugar for the next release accordingly.


Denis Bueno schrieb:
On Wed, Jul 23, 2008 at 05:27, Makarius <makarius at> wrote:
On Tue, 22 Jul 2008, Denis Bueno wrote:

I'm having a few problems formatting my theory.

- Is there a way to make syntax appear for an arbitrary definition
without changing the each use?  I thought "notation" would do this,
but my typesetting didn't change.
The Isabelle document preparation system merely presents your sources.
Only explicit antiquotations like @{term "x + y"} are printed again.

The 'notation' command allows you to write your sources in the way you
expect, but you have to do it yourself.  (The document preparation system
manages to produce quite good results without even understanding the
structure of the theory sources.)

Ah, okay, thanks for the clarification.

Is there a reason you can think of, or a procedure I might use to
debug, for why importing LaTeXsugar and OptionalSugar appear not to
affect e.g. the printing of the emptyset?  Or do I need to edit the
document, e.g. to use \<emptyset> instead of {}?

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