*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 10 Oct 2008 10:17:43 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <Pine.LNX.4.64.0810091208001.1148@macbroy20.informatik.tu-muenchen.de>*References*: <183f54960809230415x3fe54d8fv576e130a98001fae@mail.gmail.com> <1222246210.3005.18.camel@weber> <48DAD6B9.2000709@rsise.anu.edu.au> <48DC4817.20205@in.tum.de> <48EC5454.5060706@rsise.anu.edu.au> <Pine.LNX.4.64.0810081122560.15844@macbroy20.informatik.tu-muenchen.de> <48ED47EC.4040006@rsise.anu.edu.au> <Pine.LNX.4.64.0810091208001.1148@macbroy20.informatik.tu-muenchen.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Makarius wrote:

On Thu, 9 Oct 2008, Jeremy Dawson wrote:Does this mean that all the functions involving an implicit context willdisappear? eg, Simp_tac, simpset, etc ? My code is full of these.Simp_tac and simpset: unit -> simpset are indeed legacy features, too,although not explicitly marked as such. When embedding ML into Isar prooftext, say via the method called "tactic", you can refer to the simpsetfrom the context via the @{simpset} antiquotation.Makarius

Makarius,

Regards, Jeremy

**References**:**Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)***From:*Jeremy Dawson

**Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)***From:*Makarius

**Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)***From:*Jeremy Dawson

**Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)***From:*Makarius

- Previous by Date: Re: [isabelle] how to proof some lemmas containing "\<Sum>"?
- Next by Date: [isabelle] Sledgehammer in FOL
- Previous by Thread: Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
- Next by Thread: [isabelle] how to proof some lemmas containing "\<Sum>"?
- Cl-isabelle-users October 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