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



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 {}?

-- 
 Denis





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