Re: [isabelle] Lifting variables in theorem



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?

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?

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

Jeremy







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