[isabelle-dev] Symmetric difference of sets

[mailing-list anonymous]

Dear All,

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.

Also, I would highly appreciate if you could elaborate on the following: "I
would never use an abbreviation here, due to the repetition of variables".
I would like to understand what could be the potential pitfalls of using an
abbreviation in this case.

Thank you

-- 
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190919/94b6c287/attachment.html>