# HG changeset patch
# User wenzelm
# Date 760712918 -3600
# Node ID 443dc2c3758378b49e12140ab9e44adecdf915f4
# Parent  ca6eb7e6e94f74c7577883db39e03f35d727e832
added eq_set;

diff -r ca6eb7e6e94f -r 443dc2c37583 src/Pure/library.ML
--- 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)