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 Drule.export_without_context.

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.


	Makarius


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