Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Scalable operations for Thm.instanti...

view this post on Zulip Email Gateway (Sep 22 2021 at 10:32):

From: Makarius <>
* ML *

This refers to Isabelle/4974c3697fee.

Many years ago, I made measurements that showed that the naive association
lists were actually sufficient for most applications. Now I did change my mind
and made it more scalable: the impact is hardly measurable, apart from
where there is a clear reduction of runtime.

That example also shows that more heap space is required: 2-3 trees require
more overhead than plain list.

Right now I am inclined to leave this new status-quo, unless someone comes
with concrete applications that require further tuning (e.g. a different
implementation behind the now abstract data types of Vars.table etc.)


isabelle-dev mailing list

Last updated: Mar 04 2024 at 10:08 UTC