Yes, I’d be happy with that, and specifically with ∃⇩≤⇩1 + standard keyboard abbreviation.
Cheers, Gerwin > On 11 May 2020, at 00:56, Lawrence Paulson <[email protected]> wrote: > > It would be great if we could finalise the proposal for the uniqueness > quantifier. > > I was planning to do this in a strictly upward compatible way, so with no > implications for the existing quantifier notations and no changes to existing > theorems, but a few new theorems. For that I think that "∃⇩≤⇩1” is a standard > notation and works well enough. The notation “∃!” for unique existence is > also absolutely standard and surely does not need to change. > > Larry > >> On 2 May 2020, at 18:17, Makarius <[email protected]> wrote: >> >> In contrast, the other idea "∃⇩≤⇩1" from Mathoverflow would come out for Ex1 >> as "∃⇩=⇩1" or "∃⇩1", and thus introduce an incoherence of notation. >> > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
