[isabelle-dev] Symmetric difference of sets

[Lawrence Paulson]

> On 19 Sep 2019, at 14:56, mailing-list anonymous <mailing.list.anonymous at gmail.com> wrote:
> 
> 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. 

Just the obvious one: you are making multiple copies of the operand, which could lead to exponential growth if the operator is nested.

Larry