Re: [isabelle] Lifting variables in theorem



On Sat, 1 Feb 2014, Jeremy Dawson wrote:

I don't know about recent versions of Isabelle, but in Isabelle2005 the function Drule.standard does this (plus some other useful things).

I see subsequent emails in the thread talk about contexts - again I don't know about subsequent versions of Isabelle, but in Isabelle 2005 contexts (as I understand the way the word is used nowadays) are not part of a theorem.

No, Isabelle2005 has the same notion of global background context (type "theory") and local proof context (type "Proof.context"), it also has locales and other applications of local context routinely available. The thing that is part of the thm is merely a certificate of the background theory, not a proper context. (It is merely a historical accident that the certificate also contains the full background theory content, not just its identification stamp.)

Drule.standard was already disruptive to local situations in Isabelle2005, but many more tools were not properly localized, so it did not stand out particularly.

Starting with Isabelle2007, old things were systematically removed under the label of "localization". That is a long story and still not finished, but the system is continously converging to a fully local context 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-ies were removed. This is the deeper reason why you are yourself still stuck with it, since it is possible to pretend that it is Isabelle98.

Consequently we have every few months a thread on this mailing list to uncover features of historic Isabelle versions that hardly anybody remembers anymore.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.