*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Lifting variables in theorem*From*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Date*: Mon, 3 Feb 2014 22:16:37 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1402031101490.45524@lxbroy10.informatik.tu-muenchen.de>*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>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130110 Thunderbird/17.0.2

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 runproofs today which were written in 2005 (or, indeed, much earlier).That problem is de-facto solved since 2004: Isabelle/AFPhttp://afp.sf.netYou merely need to put your material into shape (according to minimalstandards that are routine today) and submit it to the editors of thearchive. Afterwards it is usually maintained "automagically" to workwith current Isabelle versions, but in extreme cases the editors mightask for you for assistance.

Hi Makarius,

If I'm wrong about this, please clarify Cheers, Jeremy

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

**Re: [isabelle] Lifting variables in theorem***From:*Lars Noschinski

**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

- Previous by Date: Re: [isabelle] [Coq-Club] Large bodies of knowledge
- Next by Date: Re: [isabelle] Lifting variables in theorem
- 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