[isabelle-dev] Symmetric difference of sets

Lawrence Paulson lp15 at cam.ac.uk
Thu Sep 19 16:04:53 CEST 2019

> 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.


More information about the isabelle-dev mailing list