[isabelle-dev] Symmetric difference of sets
mailing.list.anonymous at gmail.com
Thu Sep 19 15:56:49 CEST 2019
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.
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...
More information about the isabelle-dev