Re: [isabelle] Lifting variables in theorem

On 04.02.2014, at 10:27 am, Jeremy Dawson <Jeremy.Dawson at> wrote:

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

In exceptional situations yes. Otherwise, we prefer structured Isar over apply style, but do not mandate it. Currently about 3% of the files in the AFP are ML (50 out of 1663, 6 files use ML embedded in .thy).

> Is the person in charge of it reading this thread?  Who is in charge of it?

Google "archive of formal proofs editors":

"The editors of the archive are

        • Gerwin Klein, National ICT Australia
        • Tobias Nipkow, Technische Universität München
        • Larry Paulson, University of Cambridge"

> Is Isar-2005 code acceptable or does it have to be Isar-2014?  If the latter,
> are there conversion guides between consecutive versions, which the AFP
> maintainers used?

Submissions must work with the current Isabelle release version (currently 2013-2).

In exceptional circumstances (e.g. just before the next Isabelle release or similar), submissions for the current development version may be accepted, but they will not be listed on the front page until that Isabelle release comes out.

Older Isabelle versions are not accepted.

The rationale is that users should be able to download any AFP entry with the current Isabelle release and have everything work out of box. Entries are maintained to stay current over time.

> What are the minimal standards referred to by Makarius in his earlier post?

For the AFP:



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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