*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] antiquotations*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 07 Mar 2008 14:11:24 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <Pine.LNX.4.64.0802141321090.8150@atbroy99.informatik.tu-muenchen.de>*References*: <478AAC94.3030404@rsise.anu.edu.au> <478B2940.5020107@informatik.tu-muenchen.de> <478BEE3B.2000007@rsise.anu.edu.au> <478C8265.2010202@in.tum.de> <478D322C.7010001@rsise.anu.edu.au> <478DB7F0.7080604@in.tum.de> <478E6F17.9000100@rsise.anu.edu.au> <478E816D.9010606@in.tum.de> <478EF53A.9070809@rsise.anu.edu.au> <Pine.LNX.4.63.0801241542360.18967@atbroy100.informatik.tu-muenchen.de> <47ABC81B.3090608@rsise.anu.edu.au> <Pine.LNX.4.63.0802081405450.9643@atbroy100.informatik.tu-muenchen.de> <47AF877C.4050205@rsise.anu.edu.au> <47B04E56.7010901@in.tum.de> <47B381D7.7050908@inf.ed.ac.uk> <47B3A61F.5090907@rsise.anu.edu.au> <Pine.LNX.4.64.0802141321090.8150@atbroy99.informatik.tu-muenchen.de>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Makarius wrote: In relation to advocating the use of antiquotations, you said:

It is determined from the context :-)Pointing your finger at a particular position in Isar source text, youdetermine a certain context once and for all. Any embedded ML code atthat point will keep this as a first-class value (of type Proof.context)for later use at run-time; provided proper antiquotations are used. Sothis is just the well-known static closure principle applied toIsabelle/Isar + embedded ML.In contrast, low-level access to global references buys you dynamicscoping in the best case, and erratic non-determinism in the worst case.This is why thm"foo", thms"foo", the_context() are all bad.Makarius

(this was in relation to advocating the use of antiquotations)

Exception- ERROR "Stale theory encountered:\n{ProtoPure, Pur (etc) When I change this back to the_context () the error goes away. What is a stale theory, and why does @{theory} produce a stale theory? Jeremy Dawson

**Follow-Ups**:**Re: [isabelle] antiquotations***From:*Makarius

- Previous by Date: [isabelle] Pdf generation
- Next by Date: [isabelle] Two new AFP entries: Simpl and BDD
- Previous by Thread: Re: [isabelle] Pdf generation
- Next by Thread: Re: [isabelle] antiquotations
- Cl-isabelle-users March 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