Scalable operations for Thm.instantiate and Thm.generalize
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.
- Projects
- None
- Subscribers
- None