[isabelle] Instantiating a quantifier in a tactic


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?



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