[isabelle-dev] Symmetric difference of sets

[mailing-list anonymous]

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 <lp15 at cam.ac.uk> wrote:

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

-- 
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190919/707ccd3a/attachment.html>