[isabelle-dev] ML equality types

[Makarius]

On Thu, 10 Sep 2015, Florian Haftmann 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

These operations are a bit old-fashioned, but why are they discouraged?

As far as I know, David Matthews is doing a dictionary construction 
internally (for some years already).  So it is just a minimal form of 
Haskell-style type-class discipline.


 	Makarius