Re: [isabelle] Finding the instantiation of a variable
On Thu, Jul 8, 2010 at 3:38 PM, Steve W <s.wong.731 at gmail.com> wrote:
> Does anyone know how one would go about finding the instantiation of a
> variable in ML? Say, if I can obtain the proof term for the theorem 'EX f x.
> f x > 0', how do I work with the proof term in order to find the
> instantiations of 'f' and 'x'?
Would the first step be to reconstruct the proof using
Reconstruct.reconstruct_proof? If so, what would subsequent steps involve?
Any help will be appreciated.
This archive was generated by a fusion of
Pipermail (Mailman edition) and