improved Monitor_Dockable, based on ML_Statistics operations; tuned signature;

get rid of two-year-old hack, now that the "metis" skolemizer no longer gets stuck in HO unification

avoid explosion in higher-order unification algorithm

avoid repeated calls to metis from "resolve_tac" in case of ultimate failure

tuned comment

merged

added standard_frames convenience;

some grouping of standard fields; tuned signature;

some support for chart drawing;

some support for ML statistics content interpretation;

moved files;

moved files;

ML runtime statistics: read properties from build log;

support File.read_gzip as well, in accordance to File.write_gzip; tuned signature;

inline ML statistics into build log;

removed outdated comment;

enable Z3 for full test (cf. 6f48853f08d5);

removed old, unused code

removed whitespace

removed duplicate code

use rpair to avoid swap

generate "obtain" steps corresponding to skolemization inferences

keep E's and Vampire's skolemization steps

tuning

fixed oversensitive Skolem handling (cf. eaa540986291)

added "obtain" to Isar proof construction data structure

tuning

properly take the existential closure of skolems

use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)

tuning