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