*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)*From*: Makarius <makarius at sketis.net>*Date*: Thu, 9 Oct 2008 12:09:34 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <48ED47EC.4040006@rsise.anu.edu.au>*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>

On Thu, 9 Oct 2008, Jeremy Dawson wrote: > Does this mean that all the functions involving an implicit context will > disappear? 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 proof text, say via the method called "tactic", you can refer to the simpset from the context via the @{simpset} antiquotation. Makarius

**Follow-Ups**:

**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

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