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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
