Re: [isabelle] Instantiating a quantifier in a tactic
On 09/24/2010 02:27 AM, John Munroe wrote:
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?
I think it should be
res_inst_tac [("x", "c")] exI 1
This archive was generated by a fusion of
Pipermail (Mailman edition) and