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.
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 <[email protected]> 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
