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

Reply via email to