I use those frequently as a curried version of 'op =', e.g. 'filter (equal "..." o fst) ...'.
Lars Le 10 septembre 2015 12:31:14 GMT+02:00, Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> a écrit : >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
