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 <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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to