[isabelle-dev] ML equality types
lp15 at cam.ac.uk
Thu Sep 10 12:51:33 CEST 2015
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.
> 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?
> PGP available:
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev