[isabelle-dev] [isabelle] Tiny minor backward-compatible changes to IFOL

Klein, Gerwin (Data61, Kensington NSW) Gerwin.Klein at data61.csiro.au
Mon May 11 10:18:28 CEST 2020

Yes, I’d be happy with that, and specifically with ∃⇩≤⇩1 + standard keyboard abbreviation.


> On 11 May 2020, at 00:56, Lawrence Paulson <lp15 at cam.ac.uk> 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 <makarius at sketis.net> 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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list