[isabelle-dev] not-exists problem

Lawrence Paulson lp15 at cam.ac.uk
Tue Sep 13 23:33:35 CEST 2016

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


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

More information about the isabelle-dev mailing list