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.


 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.

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.

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 forget here.


	Makarius




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