Re: [isabelle] Lifting variables in theorem



On Fri, 31 Jan 2014, Makarius wrote:

 but as this raises an error when the tactic fails it doesn't quite fit.

I don't understand that. It seems to refer implicitly to a particular approach used here. Do you want to use local variables within a tactic?
Then just fix them, and export whatever you prove, and they become schematic.

Moa, if you have any further questions, you are wolcome. Maybe just open another thread, so that the carnival session can continue undisturbed here. (The original question was not about "lifting variables" anyway.)


	Makarius




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