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

Makarius makarius at sketis.net
Mon Apr 27 13:49:05 CEST 2020


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


More information about the isabelle-dev mailing list