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;

more robust treatment of UTF8 in raw byte sources;

clarified check, assuming that load commands are plain ASCII;

more documentation;

disallow blanks, relevant for session_name / theory_name e.g. in build log files;

uniform system name;

store session sources stamp;

generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen

misc tuning and modernization;

tuned output;

discontinued Linux 32bit platform support;

obsolete;

merged

updated to jdk-8u152, which is for x86_64 only;

added lemma

minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;

tuned output;

updated test version;

merged

auto update;

more recent polyml-test version;

parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);

tuned;

clarified signature;

tuned: build hg_graph only once; tuned signature;

tuned

derived axiom iffI as a lemma (thanks to Alexander Maletzky)

remove trailing whitespaces in List

drop a superfluous assumption that was found by the find_unused_assms command

drop a superfluous assumption that was found by the find_unused_assms command and tune proof

drop a superfluous assumption that was found by the find_unused_assms command and tune proof

algebraic foundation for congruences

more ambitious test;

added lemmas and tuned proofs

merged

Switching to inverse image and constant_on, plus some new material

proper integer option for Admin/build_history;

clarified output;

tuned output;

more thorough treatment of afp_version and afp_pull_date;

tuned options;

tuned output;

uniform execute, with proper isabelle_identifier (notably for "isabelle components -I");

tuned;

permissive theory_timings for historic versions;

store theory timings in session in build_log database; tuned;

provide theory timing information, similar to command timing but always considered relevant;

tuned;

init user settings on fresh test machine;

added [simp]

proper value;

more AFP tests;

added ml_statistics_step to trim stored properties;

proper argument;

tuned (graph.all_succs already contains origin);

support for AFP versions; added AFP tests: non-slow, two partitions;

clarified afp_pull_date: both repository versions are relevant;

clarified stored build_args;

partition AFP sessions according to structure, which happens to cut it roughly into equal parts;

support for AFP in build_history and remote_build_history;

tuned whitespace;

support for AFP versions;

tuned signature;

tuned signature;

support for AFP versions;

tuned;

added lemmas, tuned spaces

entries_graph requires acyclic graph, but lazy val allows forming the AFP object nonetheless;

more informative Imports.Report with actual session imports (minimized);

more robust: allow URLs;

more robust: allow Windows file names;