[isabelle] Obtaining the instantiation of variables in a proof



Hi all,

Given the trivial proof for EX x. x >' 0' by using the axiom 1' >' 0', is
there a way to see by which term x is instantiated (by 1' in this case)? Can
this be done in PG? If not, how can this be done in ML?

Thanks

Steph




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