When mathematicians use such notations, they are communicating informally and
they can count on the reader to understand what they mean. But that’s not how
it works for us. Any notation that could be misinterpreted should be input only
(assuming we support it at all). That way, the user immediately sees how it was
> On 13 Sep 2016, at 11:27, Manuel Eberl <ebe...@in.tum.de> wrote:
> The desired multi-variable semantics of ∄ seem obvious enough to me and I
> think that this should be allowed.
> For ∃!, the implicit complexity introduced by the pairing seems too much to
> me, so I think this should be forbidden.
isabelle-dev mailing list