Re: [isabelle] Stuck with existential quantifier
- To: isabelle-users at cl.cam.ac.uk
- Subject: Re: [isabelle] Stuck with existential quantifier
- From: Christian Kühnel <christian.kuehnel at gmail.com>
- Date: Mon, 25 Jul 2011 22:17:39 +0200
- In-reply-to: <CAMUB54ooDq7bVfzk5Pub33bfpuKKe3beg+pJwhUeSen_F5zoPQ@mail.gmail.com>
- References: <CAMUB54ooDq7bVfzk5Pub33bfpuKKe3beg+pJwhUeSen_F5zoPQ@mail.gmail.com>
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and