--- a/src/Pure/library.ML Thu Oct 22 16:52:06 2009 +0200
+++ b/src/Pure/library.ML Thu Oct 22 16:58:22 2009 +0200
@@ -174,6 +174,7 @@
(*lists as multisets*)
val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
+ val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
(*orders*)
val is_equal: order -> bool
@@ -863,6 +864,9 @@
fun combine eq xs ys = fold (remove1 eq) ys xs @ ys;
+fun submultiset _ ([], _) = true
+ | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);
+
(** orders **)