*To*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Subject*: Re: [isabelle] Lifting variables in theorem*From*: Makarius <makarius at sketis.net>*Date*: Mon, 3 Feb 2014 12:47:07 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <52EF7A95.4030505@anu.edu.au>*References*: <4B8F827F-81E0-4526-A3C3-07D35B11E013@chalmers.se> <52EC64E4.30405@anu.edu.au> <alpine.LNX.2.00.1402011236190.15165@lxbroy10.informatik.tu-muenchen.de> <52ED0D37.1070908@anu.edu.au> <alpine.LNX.2.00.1402011914460.25155@lxbroy10.informatik.tu-muenchen.de> <52EE6127.7080707@anu.edu.au> <alpine.LNX.2.00.1402031101490.45524@lxbroy10.informatik.tu-muenchen.de> <52EF7A95.4030505@anu.edu.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 3 Feb 2014, Jeremy Dawson wrote:

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 notto be true. Unless (in this case), your "minimal standards" meansrewriting everything in Isar. Which, as my previous email pointed out,is not on, since I'm guessing my latest effort involves three to fourhundred thousand tactic applications.If I'm wrong about this, please clarify

Makarius

**References**:**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**Re: [isabelle] Lifting variables in theorem***From:*Makarius

**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**Re: [isabelle] Lifting variables in theorem***From:*Makarius

**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

**Re: [isabelle] Lifting variables in theorem***From:*Makarius

**Re: [isabelle] Lifting variables in theorem***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] Lifting variables in theorem
- Next by Date: Re: [isabelle] [Coq-Club] Large bodies of knowledge
- Previous by Thread: Re: [isabelle] Lifting variables in theorem
- Next by Thread: Re: [isabelle] Lifting variables in theorem
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list