*To*: Denis Bueno <dbueno at gmail.com>*Subject*: Re: [isabelle] A few questions about LaTeX theory output*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 25 Jul 2008 12:22:40 +0200*Cc*: isabelle-users at cl.cam.ac.uk, Makarius <makarius at sketis.net>*In-reply-to*: <6dbd4d000807240705m49ddc801s215b4119b562540b@mail.gmail.com>*References*: <6dbd4d000807220958y5632371dy3758fd2e54983995@mail.gmail.com> <Pine.LNX.4.64.0807231124200.28573@macbroy20.informatik.tu-muenchen.de> <6dbd4d000807240705m49ddc801s215b4119b562540b@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.9 (Macintosh/20071031)

Replace syntax (latex output) "_emptyset" :: "'a set" ("...") translations "_emptyset" <= "{}" by 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. Tobias Denis Bueno schrieb:

On Wed, Jul 23, 2008 at 05:27, Makarius <makarius at sketis.net> 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 {}?

**References**:**[isabelle] A few questions about LaTeX theory output***From:*Denis Bueno

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

**Re: [isabelle] A few questions about LaTeX theory output***From:*Denis Bueno

- Previous by Date: Re: [isabelle] Using case_tac with functions that have not been exhaustively defined
- Next by Date: [isabelle] new AFP entry: SATSolverVerification
- Previous by Thread: Re: [isabelle] A few questions about LaTeX theory output
- Next by Thread: [isabelle] Using case_tac with functions that have not been exhaustively defined
- Cl-isabelle-users July 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list