# HG changeset patch
# User wenzelm
# Date 1681289570 -7200
# Node ID 9d124714a9e85599e5a5f43d1b7583c28bef4702
# Parent  c18c0dbefd55b7f3d9da254c056f50dcb024e3aa
more operations;

diff -r c18c0dbefd55 -r 9d124714a9e8 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Wed Apr 12 10:42:23 2023 +0200
+++ b/src/Pure/General/set.ML	Wed Apr 12 10:52:50 2023 +0200
@@ -23,6 +23,7 @@
   val get_first: (elem -> 'a option) -> T -> 'a option
   val member: T -> elem -> bool
   val subset: T * T -> bool
+  val eq_set: T * T -> bool
   val ord: T ord
   val insert: elem -> T -> T
   val make: elem list -> T
@@ -278,6 +279,9 @@
 
 fun subset (set1, set2) = forall (member set2) set1;
 
+fun eq_set (set1, set2) =
+  pointer_eq (set1, set2) orelse size set1 = size set2 andalso subset (set1, set2);
+
 val ord =
   pointer_eq_ord (fn sets =>
     (case int_ord (apply2 size sets) of