> On 13.09.2016, at 23:33, Lawrence Paulson <l...@cam.ac.uk> wrote:
> 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 ∄.
But to what extent do you find it confusing? Perhaps because our brains are
damaged by too much logic and too little math, many of us on this list seemed
to have no real issues parsing your example correctly.
isabelle-dev mailing list