changeset 4363 | b449831f03f4 |
parent 4343 | 9849fb57c395 |
child 4445 | de74b549f976 |
--- a/src/Pure/library.ML Thu Dec 04 13:49:27 1997 +0100 +++ b/src/Pure/library.ML Thu Dec 04 13:49:51 1997 +0100 @@ -514,6 +514,10 @@ fun ([]:string list) subset_string ys = true | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys; +(*set equality*) +fun eq_set (xs, ys) = + xs = ys orelse (xs subset ys andalso ys subset xs); + (*set equality for strings*) fun eq_set_string ((xs:string list), ys) = xs = ys orelse (xs subset_string ys andalso ys subset_string xs);