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:

> Hi,
>
> 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.

Thanks
Steve

Thanks
> Steve
>




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