On 13/09/16 01:46, Lawrence Paulson wrote:
> We have a problem with the ∄ operator, when existential quantifiers are
> 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.
isabelle-dev mailing list