*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] antiquotations*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 08 Feb 2008 14:10:19 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <Pine.LNX.4.63.0801241542360.18967@atbroy100.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>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Makarius wrote:

Having studied the recent threads on the "effect of use_thy","antiquotations" etc. here is a summary in my own words, together withsome additional hints on how to avoid problems with old ways of doingthings, and moving on towards more powerful concepts.* The raw interactive ML toplevel is mostly obsolete. After many yearsof the two toplevels side-by-side, we have finally passed the turningpoint where everything is Isar, and ML is smoothly integrated intothat. Proper context-dependent antiquotations are just one benefitfrom this principle, and typing additional ML {* *} should be a smallprice to pay in current Proof General (adding a key binding to producethat wrapping should be trivial anyway).

The latest example is contained in the attached theory file.

Why is this? I suspect it is to do with theories, and noted that

from the result it gives afterwards. Why is this?

* ML functions that refer to the old-style (dynamic) context, such as"the_context" and "thm" are very hard to understand exactly and shouldbe replaced more and more by proper antiquotations (which arestatically scoped at compile-time).

So far as I understood the previous emails,

Anyway, attached is the theory file that has taken so much of my time.

Regards, Jeremy Dawson

**Follow-Ups**:**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Makarius

- Previous by Date: [isabelle] CALL FOR BIDS (TPHOLs'2009)
- Next by Date: Re: [isabelle] antiquotations
- Previous by Thread: [isabelle] CALL FOR BIDS (TPHOLs'2009)
- Next by Thread: Re: [isabelle] antiquotations
- Cl-isabelle-users February 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