added eq_set;

--- a/src/Pure/library.ML	Fri Feb 04 10:32:27 1994 +0100
+++ b/src/Pure/library.ML	Tue Feb 08 14:08:38 1994 +0100
@@ -439,6 +439,12 @@
 fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
 
 
+(*eq_set*)
+
+fun eq_set (xs, ys) =
+  xs = ys orelse (xs subset ys andalso ys subset xs);
+
+
 (*removing an element from a list WITHOUT duplicates*)
 infix \;
 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)