*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] LateXsugar broken?*From*: Christian Doczkal <c.doczkal at stud.uni-saarland.de>*Date*: Sun, 05 Apr 2009 18:07:18 +0200*In-reply-to*: <49D5B97C.9060206@in.tum.de>*References*: <1238592399.7341.34.camel@laptop> <49D4B515.3040406@in.tum.de> <1238677721.13378.4.camel@laptop> <49D5B97C.9060206@in.tum.de>

Hello > >> Replace the "term" command by an antiquotation, eg > >> > >> text{* @{term "if a then b else c"} *} [...] > I'm afraid that is not possible. What is the fundamental difference between rendering a term in the theory as latex output and rendering a term in an antiquotation as latex output? I was expecting that both use the same mechanisms. -- Regards Christian Doczkal

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] LateXsugar broken?***From:*Tobias Nipkow

**Re: [isabelle] LateXsugar broken?***From:*Makarius

**References**:**[isabelle] LateXsugar broken?***From:*Christian Doczkal

**Re: [isabelle] LateXsugar broken?***From:*Tobias Nipkow

**Re: [isabelle] LateXsugar broken?***From:*Christian Doczkal

**Re: [isabelle] LateXsugar broken?***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Defining Real numbers axiomatically
- Next by Date: [isabelle] Re2: how to transform *.thy to *.pdf in Isabelle?
- Previous by Thread: Re: [isabelle] LateXsugar broken?
- Next by Thread: Re: [isabelle] LateXsugar broken?
- Cl-isabelle-users April 2009 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