Re: [isabelle] Stuck with existential quantifier



>
> Dear isabelle users,

>
I'm trying to prove this obvious lemma:

>
  "~ (EX t. [1::nat,1,1] ! t = 0 )"

>
I've been trying for a while but could not figure it out. Can you please
give me a hint, how I can prove this?

>
Is there more documatation on prooving terms with existential and universal
quantifiers? The isabelle tutorial did not help me there.

>

Best regards,
Christian Kühnel




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