[isabelle-dev] NEWS: Scalable operations for Thm.instantiate and Thm.generalize

[Makarius]

*** ML ***

* ML structures TFrees, TVars, Frees, Vars, Names provide scalable
operations to accumulate items from types and terms, using a fast
syntactic order. The original order of occurrences may be recovered as
well, e.g. via TFrees.list_set.

* Thm.instantiate, Thm.generalize and related operations require
scalable datastructures from structure TVars, Vars, Names etc.
INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate
adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
accumulation of items.


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
https://isabelle.sketis.net/devel/build_status/macOS_11_Big_Sur_4_threads/index.html#session_HOL-Record_Benchmark
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.)


	Makarius