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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and