*To*: Moa Johansson <moa.johansson at chalmers.se>*Subject*: Re: [isabelle] Lifting variables in theorem*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Fri, 31 Jan 2014 17:42:17 +0100*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <0F16D9FB-EC0D-49DB-9A56-8B364574EA05@gmail.com>*References*: <4B8F827F-81E0-4526-A3C3-07D35B11E013@chalmers.se> <0F16D9FB-EC0D-49DB-9A56-8B364574EA05@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Am 31.01.2014 17:28, schrieb Jasmin Blanchette:

Hi Moa, Am 31.01.2014 um 17:11 schrieb Moa Johansson <moa.johansson at chalmers.se>:I'm currently porting some functionality from the HipSpec lemma discovery system into Isabelle.Great!Seems like this should be quite simple to do, perhaps this is what Thm.generalize is for? If so, what are its expected arguments? Seems like the first two are lists of all the type-variable and variable names we want to lift, but what is the int?You might want to have a look at "Drule.generalize". It provides a slightly higher-level interface, without the mysterious "int".

Hi Moa,

Proof_Context.export names_ctxt ctxt

Dmitriy

**References**:**[isabelle] Lifting variables in theorem***From:*Moa Johansson

**Re: [isabelle] Lifting variables in theorem***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Lifting variables in theorem
- 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 January 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