# HG changeset patch
# User wenzelm
# Date 1688221966 -7200
# Node ID f3a6140fa3b178399c8c079b5c0c6b265f08cc79
# Parent  aece9a0632718bf9125ba5f5d0c91c774f90aaa2
tuned signature: more operations;

diff -r aece9a063271 -r f3a6140fa3b1 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Sat Jul 01 16:27:34 2023 +0200
+++ b/src/Pure/General/sha1.scala	Sat Jul 01 16:32:46 2023 +0200
@@ -65,6 +65,8 @@
 
     def is_empty: Boolean = rep.isEmpty
 
+    def - (other: Shasum): Shasum = new Shasum(rep.filterNot(other.rep.toSet.contains))
+
     def :::(other: Shasum): Shasum = new Shasum(other.rep ::: rep)
 
     def filter(pred: String => Boolean): Shasum = new Shasum(rep.filter(pred))