[isabelle-dev] not-exists problem

Tjark Weber tjark.weber at it.uu.se
Tue Sep 13 10:41:39 CEST 2016

On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> I would have expected:
> (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> and
> (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))



More information about the isabelle-dev mailing list