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

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.


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