# HG changeset patch
# User wenzelm
# Date 754567697 -3600
# Node ID 80ccb6c354ba0a5c603598bac0aab708da90fdfc
# Parent  3d0324f9417b0d81995eac57400771aec7352dc4
added equal, not_equal: ''a -> ''a -> bool

diff -r 3d0324f9417b -r 80ccb6c354ba src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Nov 26 16:35:38 1993 +0100
+++ b/src/Pure/library.ML	Mon Nov 29 11:08:17 1993 +0100
@@ -36,6 +36,14 @@
   in boolf end;
 
 
+(** curried equality **)
+
+fun equal x y = (x = y);
+
+fun not_equal x y = x <> y;
+
+
+
 (*** Lists ***)
 
 exception LIST of string;