<html><head></head><body>I use those frequently as a curried version of 'op =', e.g. 'filter (equal "..." o fst) ...'.<br>
<br>
Lars<br><br><div class="gmail_quote">Le 10 septembre 2015 12:31:14 GMT+02:00, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> a écrit :<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<pre class="k9mail">In src/Pure/library.ML, the signature still contains the discouraged and<br />nowadays rarely used entries<br /> <br /> val equal: ''a -> ''a -> bool<br /> val not_equal: ''a -> ''a -> bool<br /><br />Shall we attempt to get rid of them finally?<br /><br /> Florian<br /></pre></blockquote></div></body></html>