*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] Antiquotation for theorem names*From*: Makarius <makarius at sketis.net>*Date*: Fri, 26 Mar 2010 11:25:51 +0100 (CET)*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4BAA1F76.1020106@uibk.ac.at>*References*: <4BAA1F76.1020106@uibk.ac.at>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Wed, 24 Mar 2010, Christian Sternagel wrote:

In isar-ref, I found the antiquiation @{theory A}, where 'A' is guaranteed torefer to a valid ancestor theory. Is the same available for theorem names,that is, something like:@{lemmas l1 ... lN} where 'l1' to 'lN' are guaranteed to be the names ofexisting lemmas and the result after document preparation is for example

Makarius

**References**:**[isabelle] Antiquotation for theorem names***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] How do I retrieve the mixfix syntax of a constant?
- Next by Date: [isabelle] Specification depends on extra type variables
- Previous by Thread: [isabelle] Antiquotation for theorem names
- Next by Thread: [isabelle] Antiquotation for Theorem Names
- Cl-isabelle-users March 2010 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