*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Lifting variables in theorem*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Mon, 03 Feb 2014 16:03:51 +0100*In-reply-to*: <52EF7A95.4030505@anu.edu.au>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20131103 Icedove/17.0.10

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

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

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

- Previous by Date: Re: [isabelle] [Coq-Club] Large bodies of knowledge
- Next by Date: [isabelle] Curious failure of simp when goal equation is reoriented
- 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