<div dir="ltr"><div>Dear All,<div><br></div><div>In the unlikely case that you are not aware, I would like to mention that there exists a definition of the xor operator in HOL-Library.Boolean-Algebra. Personally, I would like to see the theorems/definitions similar to the ones stated in HOL-Library.Boolean-Algebra to find their way to the classes in Main: it feels slightly awkward to have to use two distinct representations of Boolean algebras merely to obtain the fundamental theorems associated with the symmetric difference of sets.</div><div><br></div><div>Also, I would highly appreciate if you could elaborate on the following: "<span style="color:rgb(0,0,0);white-space:pre-wrap">I would never use an abbreviation here, due to the repetition of variables</span>". I would like to understand what could be the potential pitfalls of using an abbreviation in this case. </div><div><br></div><div>Thank you</div></div><div><br></div>-- <br><div dir="ltr" class="m_-7804319551246772605m_949804372958824956m_-2375628459503249820gmail_signature" data-smartmail="gmail_signature"><div dir="ltr">Please accept my apologies for posting anonymously. This is done to protect my privacy. I can make my identity and my real contact details available upon request in private communication under the condition that they are not to be mentioned on the mailing list.  </div></div></div>