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

[Tobias Nipkow]

On 03/05/2020 12:14, Lawrence Paulson wrote:
> On 3 May 2020, at 01:09, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein at data61.csiro.au> wrote:
> 
>> I use ! all the time, esp for input (but not only for input). It’s just so much quicker to type.
> 
> Agree. We can’t repurpose (!) and there’s no need.
> 
>> As I said already privately, there should then definitely be an
>> abbreviation for entering ∃⇩≤⇩1 using autocomplete.
> 
> I could live with that… I use abbreviations all the time.

I agree. The "∃⇩≤⇩1" notation is very natural, it was suggested on Mathoverflow 
and it corresponds to the counting quantifiers.

Tobias

> Larry
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200503/1960e181/attachment.bin>