[isabelle] Instantiating a quantifier in a tactic



Hi,

I have a quick question regarding instantiating a quantifier
explicitly in a tactic. For example, how would the following line be
translated into a tactic:

lemma "EX z. z > a"
apply (rule exI [where x = "c"])
..

where a and c are constants. Would Drule.instantiate need to be used?

TIA

John





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