tuned signature: more operations;

--- 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))