added eq_set;
authorwenzelm
Tue Feb 08 14:08:38 1994 +0100 (1994-02-08)
changeset 265443dc2c37583
parent 264 ca6eb7e6e94f
child 266 3fe01df1a614
added eq_set;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Feb 04 10:32:27 1994 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Feb 08 14:08:38 1994 +0100
     1.3 @@ -439,6 +439,12 @@
     1.4  fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
     1.5  
     1.6  
     1.7 +(*eq_set*)
     1.8 +
     1.9 +fun eq_set (xs, ys) =
    1.10 +  xs = ys orelse (xs subset ys andalso ys subset xs);
    1.11 +
    1.12 +
    1.13  (*removing an element from a list WITHOUT duplicates*)
    1.14  infix \;
    1.15  fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)