Re: [isabelle] size entry-point in signature TABLE



> On 7 May 2015, at 19:23, Makarius <makarius at sketis.net> wrote:
>
> On Thu, 7 May 2015, Michael Norrish wrote:
>
>> 125000 live tables in memory.  Tables can get big (motivating the desire to avoid O(n) operations), but Iâd be surprised if a running Isabelle really had that many tables around.
>
> My guess is that we normally have millions of live tables around, and it is important that their substructure is sharable as much as possible.

Wow.  Thatâs a fascinating number.  Note of course that the obvious way to store table sizes would not affect sharing of substructure.

Michael

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.