Re: [isabelle] Lifting variables in theorem
On Mon, 3 Feb 2014, Jeremy Dawson wrote:
My whole point is that it should NOT be difficult for anyone to run
proofs today which were written in 2005 (or, indeed, much earlier).
That problem is de-facto solved since 2004: Isabelle/AFP http://afp.sf.net
You merely need to put your material into shape (according to minimal
standards that are routine today) and submit it to the editors of the
archive. Afterwards it is usually maintained "automagically" to work with
current Isabelle versions, but in extreme cases the editors might ask for
you for assistance.
Thus you can see old Isabelle applications from the late 1990-ies fresh
and running on Isabelle2013-2, e.g. see the 2004 edition where the
archive was started by importing material from previous years.
I'm not clear what the problem is that you are describing but it doesn't
sound like anything I have issues with in my work.
The Proof.context was introduced shortly after Isabelle98 in order to
support structured proofs in Isar. Later it turned out as generally
useful concept, so after 2000 or so, more and more tools became
context-aware. That made a big difference: before there was unsure
tinkering with free and schematic variables by hand, never being sure
if they could clash with other variables from the environment;
afterwards things actually started working reliably.
That was merely an attempt to close the circle on this thread. It started
out about proper treatment of fixed and schematic variables in Isabelle
today, using a proper Proof.context. That is quite different from the
all-global nothing-local situation in Isabelle98, which we should better
This archive was generated by a fusion of
Pipermail (Mailman edition) and