*To*: Denis Bueno <dbueno at gmail.com>*Subject*: Re: [isabelle] A few questions about LaTeX theory output*From*: Makarius <makarius at sketis.net>*Date*: Wed, 23 Jul 2008 11:27:20 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <6dbd4d000807220958y5632371dy3758fd2e54983995@mail.gmail.com>*References*: <6dbd4d000807220958y5632371dy3758fd2e54983995@mail.gmail.com>

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

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

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

- Previous by Date: Re: [isabelle] Partially terminating functions
- Next by Date: [isabelle] Using case_tac with functions that have not been exhaustively defined
- Previous by Thread: [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