Re: [isabelle] Instantiating a quantifier in a tactic



On 09/24/2010 02:27 AM, John Munroe wrote:
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

John,

I think it should be

res_inst_tac [("x", "c")] exI 1

Jeremy






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