Thanks to Phil Clayton for pointing out that the the Unicode code point 2A04 N-ARY UNION OPERATOR WITH PLUS that was being used for the Z bag union operator is really intended for a distributed union operation. The code point 228E MULTISET UNION is a more logical choice for binary bag union. I have updated the web page that describes the mapping here:
http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html <http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html> and also updated the ProofPower and pputf8 source in the github source repos: https://www.github.com/RobArthan/pp <https://www.github.com/RobArthan/pp> https://www.github.com/RobArthan/pp-contrib <https://www.github.com/RobArthan/pp-contrib> The correction will appear in the next release. Regards, Rob.
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com