[isabelle-dev] not-exists problem

[Lawrence Paulson]

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

> On 13 Sep 2016, at 11:27, Manuel Eberl <eberlm at 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.
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160913/4b12bc0e/attachment-0002.html>