Dear Lawrence Paulson, Thank you for your reply. I thought that there could be other unstated problems with this abbreviation. However, I can see how the problem that you mentioned alone warrants a new definition. I guess I must apologize for making an enquiry about something that should be, indeed, obvious for every user of the system.
Thank you On Thu, Sep 19, 2019 at 5:04 PM Lawrence Paulson <[email protected]> wrote: > > 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 > > -- 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
