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