Re: [isabelle] Obtaining the instantiation of variables in a proof
Stephy Wong wrote:
> 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?
If your goal is an EX, you can provide the witness by instantiating the
exI thm before use:
apply(rule_tac x = "1'" in exI)
Pls read Section 5.9, Quantifiers, of the Tutorial.
This archive was generated by a fusion of
Pipermail (Mailman edition) and