*To*: Denis Bueno <dbueno at gmail.com>*Subject*: Re: [isabelle] A few questions about LaTeX theory output*From*: Makarius <makarius at sketis.net>*Date*: Thu, 24 Jul 2008 16:36:44 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*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>

On Thu, 24 Jul 2008, Denis Bueno wrote: > 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 {}? The sugar only affects things printed via embedded antiquotations such as @{thm my_fact}. Regular source text really needs to be written the way it should be typeset. So yes, you will have to replace {} by \<emptyset> in the theory source, if you prefer that symbol over the other. Makarius

**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] A few questions about LaTeX theory output
- Next by Date: Re: [isabelle] Using case_tac with functions that have not been exhaustively defined
- Previous by Thread: Re: [isabelle] A few questions about LaTeX theory output
- Next by Thread: Re: [isabelle] A few questions about LaTeX theory output
- 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