# HG changeset patch
# User wenzelm
# Date 1682273753 -7200
# Node ID b83a561086d3d42fbd8ffa3e278eb357573dcdac
# Parent  10c09fb5a8741a3441fbe70e98d3e35c420950c8
more operations: following Library list operations and Ord_List.T operations;

diff -r 10c09fb5a874 -r b83a561086d3 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Sun Apr 23 19:57:40 2023 +0200
+++ b/src/Pure/General/set.ML	Sun Apr 23 20:15:53 2023 +0200
@@ -30,6 +30,9 @@
   val merges: T list -> T
   val remove: elem -> T -> T
   val subtract: T -> T -> T
+  val restrict: (elem -> bool) -> T -> T
+  val inter: T -> T -> T
+  val union: T -> T -> T
 end;
 
 functor Set(Key: KEY): SET =
@@ -464,6 +467,20 @@
 end;
 
 
+(* conventional set operations *)
+
+fun restrict pred set =
+  fold_set (fn x => not (pred x) ? remove x) set set;
+
+fun inter set1 set2 =
+  if pointer_eq (set1, set2) then set1
+  else if is_empty set1 orelse is_empty set2 then empty
+  else if size set1 < size set2 then restrict (member set2) set1
+  else restrict (member set1) set2;
+
+fun union set1 set2 = merge (set2, set1);
+
+
 (* ML pretty-printing *)
 
 val _ =