Phame Blogs Isabelle NEWS J44
Scalable operations for Thm.instantiate and Thm.generalize
- 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.
Written by makarius on Sep 22 2021, 12:08 PM.