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

isabelle-dev mailing list

Reply via email to