Rename multiset "union" into "disjoint union"
This fixes #13 (closed). Now ∪
and ∩
are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas ⊎
is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:

⊎
and∪
have different heights in my font (see⊎∪
). Is there maybe a better disjoint union symbol in unicode?  There are probably all kinds of laws about the interaction between
∪
,∩
, and⊎
, like distributivity. I did not attempt to prove a comprehensive set of such laws. 
∖
is still the operation that subtracts multiplicity. I think that's fine, since there is no sensible difference operator for multisets that matches up with the union operator.