Re: [isabelle] Lifting variables in theorem



On 02/03/2014 09:11 PM, Makarius wrote:
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.
Hi Makarius,

I've been told similar things on occasions before, and it turns out not to be true. Unless (in this case), your "minimal standards" means rewriting everything in Isar. Which, as my previous email pointed out, is not on, since I'm guessing my latest effort involves three to four hundred thousand tactic applications.

If I'm wrong about this, please clarify

Cheers,

Jeremy





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