[isabelle-dev] not-exists problem

Makarius makarius at sketis.net
Mon Sep 19 12:45:59 CEST 2016

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
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.


More information about the isabelle-dev mailing list