[isabelle-dev] not-exists problem

[Lawrence Paulson]

I’m not sure that this suggestion addresses my original problem: that the use of the negated quantifier (by an output translation, i.e., not by request) produced a confusing output. This output already contains only a single variable bound by ∄.

Larry

> On 13 Sep 2016, at 19:56, Makarius <makarius at sketis.net> wrote:
> 
> Looking briefly over this thread, my impression is that the simplest
> solution is to disallow multiple variables for
> ∄ and ∃! as well.
> 
> We already have special quantifiers like ∃x:A that cannot be repeated
> (for very basic technical reasons). This means users are used to
> non-iterated quantifiers: it should cause less surprise than extra
> syntax that is unclear.