[isabelle] Finding the instantiation of a variable



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'?

Thanks
Steve




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