Re: [isabelle] Lifting variables in theorem



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".

Cheers,

Jasmin





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