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.
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
