*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Lifting variables in theorem*From*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Date*: Tue, 4 Feb 2014 10:27:17 +1100*In-reply-to*: <52EFAFD7.7070101@in.tum.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> <52EF7A95.4030505@anu.edu.au> <52EFAFD7.7070101@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130110 Thunderbird/17.0.2

On 02/04/2014 02:03 AM, Lars Noschinski wrote:

On 03.02.2014 12:16, Jeremy Dawson wrote: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 your work can at least be put into the form lemma <name>: <prop> <proof> you can always escape to Isabelle/ML by using apply (tactic {* <some arbitrary ML code> *} done -- Lars

Well, is this acceptable for stuff submitted to the AFP? Is the person in charge of it reading this thread? Who is in charge of it?

are there conversion guides between consecutive versions, which the AFP maintainers used? What are the minimal standards referred to by Makarius in his earlier post? Jeremy

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

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

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

- Previous by Date: Re: [isabelle] 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