more operations;

clarified signature: name of standard_proof is authentic, otherwise empty;

support dummy term;

clarified signature default;

clarified signature default;

more operations for type classes;

clarified output and input of Typ/Term;

clarified oracle_proof;

obsolete;

Term_XML.Encode/Decode.term uses Const "typargs";

clarified type for recorded oracles;

clarified signature;

clarified PThm: theory_name simplifies retrieval from exports;

Indexname.toString according to string_of_vname' in ML;

clarified type Indexname, with plain value Int;
eliminated pointless cache_int;

more complete pattern match;

support for (fully reconstructed) proof terms in Scala;
proper cache_typs;

more operations: support type classes within the logic;

more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);

more general cache, also for term substructures;

more uniform Term and Term_XML modules;

more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;

tuned XML modules;

inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
tuned signature;

lambda terms with XML data representation in Scala;
avoid `class` in signature;