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

[Makarius]

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