Re: [isabelle] Unable to prove easy existential "directly"



On 07/19/2013 09:41 PM, Manuel Eberl wrote:
But be that as it may, even when one does annotate the bound variable,
".." still does not work, which then brings us back to what I said in my
first reply. :)

Yes. That's what I wanted to say with "combine our two mails". -cheers chris

For the record: I also find this behavior of ".."/"rule"/... vs. "rule_tac"/"blast"/... strange.





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