[isabelle-dev] not-exists problem
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:
date: Sun Sep 18 17:59:28 2016 +0200
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