[isabelle-dev] ML equality types

[Larry Paulson]

I can't see any specific benefit of doing this.

I still think that the next big project of this kind should be to sort out the real/of_nat mess. I’ve proposed an approach to doing it, but haven’t yet found a sufficient block of time in which executed.

Larry

> On 10 Sep 2015, at 11:31, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> In src/Pure/library.ML, the signature still contains the discouraged and
> nowadays rarely used entries
> 	
> 	val equal: ''a -> ''a -> bool
> 	val not_equal:  ''a -> ''a -> bool
> 
> Shall we attempt to get rid of them finally?
> 
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev