[isabelle-dev] not-exists problem

Lawrence Paulson lp15 at cam.ac.uk
Tue Sep 13 01:46:34 CEST 2016

We have a problem with the ∄ operator, when existential quantifiers are nested:

lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
  by (rule refl)

Note that ∄x y. P x y would be fine.


~/isabelle/Repos/src/HOL: hg id
dca6fabd8060 tip

More information about the isabelle-dev mailing list