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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and