[isabelle-dev] not-exists problem

[Makarius]

On 13/09/16 01:46, Lawrence Paulson wrote:
> 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.

Back to this thread. There is now the following change:

changeset:   63912:9f8325206465
user:        wenzelm
date:        Sun Sep 18 17:59:28 2016 +0200
files:       src/HOL/HOL.thy
description:
clarified notation: iterated quantifier is negated as one chunk;


This is rather unspectacular. Instead of the 2005 version of negating
the term operator, the resulting syntax is negated via plain translations.

Hopefully this does not cause other confusions. If there are remaining
problems, we should sort them out before the release.


	Makarius