removed obsolete ML bindings;

converted ex/MT.ML;

make HOL-ex earlier;

NAMED_CRITICAL;

removed stateful init: operations take proper theory argument;

removed dead code: const_typargs, num_typargs, init;

proper signature;

removed obsolete atp_method; ResHolClause.XXX_write_file: theory argument;

export more tactics; ResHolClause.literals_of_term: proper theory argument; removed obsolete ResClause.init, ResHolClause.init;

renamed ResAtpMethods.setup;

added at-poly-5.1-para;

added CRITICAL section markup;

updated generated file;

removed obsolete touch_all_thys;

compress: proper check_thy;

added encoding spec for jEdit;

proper signature;

proper signature; removed unused const_types_of;

turned type_lits into configuration option (with attribute);

removed set_concat_map and improved set_concat

check_deps: ensure that theory is actually present, not just update_time > 1;

tuned order

reoriented hook application order

explicit constants for overloaded definitions

dropped junk

tuned

changed floatarith lemmas

proper signature for Meson;

force: non-critical, but also non-thread-safe (potentially multiple evaluations);

removed dead code;