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.
>
> I don’t think a fancy symbol is needed for something that will be fairly
> lightly used however.
So why not put it into some library theory somewhere?
There is no need to change the presentation of the core logic, just for
another variant of quantifiers.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
