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

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.)


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