> On 19 Sep 2019, at 14:56, mailing-list anonymous > <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
