[isabelle-dev] not-exists problem

[Lawrence Paulson]

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.

Larry

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