obsolete;

tuned;

ROOT cleanup: empty 'document_files' means there is no document;

eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;

more informative timeout message, notably for build_status;

clarified: adapted to ML version;

proper order of initialization (amending 9953ae603a23);

More topological results overlooked last time

merged

New results in topology, mostly from HOL Light's moretop.ml

generalized some lemmas on multisets

rule out pathologic instances

tuned some proofs and added some lemmas

more recent polyml-test version;

reduced simp_depth_limit

generalized

reduced heap hierarchy, for potentially improved performance;

deactivated old tests;

avoid slow proofs due to simp rules from 960509bfd47e;

some concrete commands; clarified messages;

tuned signature;

more formal messages;

tuned signature;

separate JSON parser, which is slightly more general than (deprecated) scala.util.parsing.json.JSON;

more permissive;

tuned;

separate JSON lexer;

clarified command language;

use Poly/ML 5.7.1 test version as default;

more explicit check;