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

[Tobias Nipkow]

On 27/04/2020 13:08, Lawrence Paulson wrote:
> I have only recently proved a result of this sort, and thinking back, the need to write out
> 
> 	!x y. P x & P y —> x=y
> 
> has always been one of my pet bugbears.

That does indeed crop up from time to time.

Tobias

> I don’t think a fancy symbol is needed for something that will be fairly lightly used however.

> Larry
> 
>> On 27 Apr 2020, at 11:58, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>
>> 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
> 

-------------- 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/5a625b41/attachment.bin>