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

[Tobias Nipkow]

On 27/04/2020 11:23, Lawrence Paulson wrote:
> But looking more closely, the specific proposal (regardless of the implementation) is excellent: it is simply an “at most one” quantifier, which we also need in Isabelle/HOL, and I’m wondering that I didn’t grasp the need for this 30 years ago.

I don't recall feeling the need for it, although I may just be too used to what 
we have to conceive of notions beyond. But I have (almost) never seen it 
anywhere else. There are of course the counting quantifiers.

Having said that, I wouldn't object to an "at most one" quantifier provided it 
has a decent syntax. See 
https://math.stackexchange.com/questions/1205464/quantifier-for-there-is-at-most-one

Tobias

-------------- 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/20200427/aa25530d/attachment.bin>