*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Lifting variables in theorem*From*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Date*: Sun, 2 Feb 2014 02:05:27 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1402011236190.15165@lxbroy10.informatik.tu-muenchen.de>*References*: <4B8F827F-81E0-4526-A3C3-07D35B11E013@chalmers.se> <52EC64E4.30405@anu.edu.au> <alpine.LNX.2.00.1402011236190.15165@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130110 Thunderbird/17.0.2

On 02/01/2014 10:50 PM, Makarius wrote:

On Sat, 1 Feb 2014, Jeremy Dawson wrote:I don't know about recent versions of Isabelle, but in Isabelle2005the function Drule.standard does this (plus some other useful things).I see subsequent emails in the thread talk about contexts - again Idon't know about subsequent versions of Isabelle, but in Isabelle2005 contexts (as I understand the way the word is used nowadays) arenot part of a theorem.No, Isabelle2005 has the same notion of global background context(type "theory") and local proof context (type "Proof.context"), italso has locales and other applications of local context routinelyavailable. The thing that is part of the thm is merely a certificateof the background theory, not a proper context. (It is merely ahistorical accident that the certificate also contains the fullbackground theory content, not just its identification stamp.)Drule.standard was already disruptive to local situations inIsabelle2005, but many more tools were not properly localized, so itdid not stand out particularly.Starting with Isabelle2007, old things were systematically removedunder the label of "localization". That is a long story and still notfinished, but the system is continously converging to a fully localcontext displiciple for all proof tools and definitional packages.The jump from Isabelle2005 to Isabelle2007 (with 25 months distance)also marks the point where really ancient things from the 1990-ieswere removed. This is the deeper reason why you are yourself stillstuck with it, since it is possible to pretend that it is Isabelle98.Consequently we have every few months a thread on this mailing list touncover features of historic Isabelle versions that hardly anybodyremembers anymore.Makarius

Hi Makarius,

Jeremy

**Follow-Ups**:**Re: [isabelle] Lifting variables in theorem***From:*Makarius

**References**:**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**Re: [isabelle] Lifting variables in theorem***From:*Makarius

- Previous by Date: Re: [isabelle] Lifting variables in theorem
- Next by Date: [isabelle] Call for papers: Nonlinear Reasoning
- Previous by Thread: Re: [isabelle] Lifting variables in theorem
- Next by Thread: Re: [isabelle] Lifting variables in theorem
- Cl-isabelle-users February 2014 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