Re: [isabelle] Lifting variables in theorem



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





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