Re: [isabelle] Lifting variables in theorem
On Fri, 31 Jan 2014, Lawrence Paulson wrote:
I donʼt recognise much in the code any more, but you could consider
Not that one again: any of the "without_context" operations are even worse
than the "global" ones. That is anncient legacy.
We have official type Proof.context with various elementary operations to
fix variables and export results since about 1999. The "implementation"
manual explains that in section 6.1 with various examples.
This archive was generated by a fusion of
Pipermail (Mailman edition) and