polyml-test version based on experimental branch NewTestRegisterSave;

support for libgmp on x86_64-darwin;

avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;

delegate boundary cases to existing IntInf.pow;

plain identify job for Isabelle + AFP, independent of any Isabelle technology;

tuned (non-unique example);

clarified situation of global theory names;

less global theories -- avoid confusion about special cases;

proper deps;

allow unrelated ancestor; clarified error;

tuned;

support alternative ancestor session;

support focus_session, for much faster startup of Isabelle/jEdit; more options for "isabelle jedit";

more timing;

tuned;

init only once (see also c0f776b661fa);

proper merge (amending fb46c031c841);

build faster without heap images for minor imports;

proper order for entries from multiple profiles, notably "AFP";

tuned output;

tuned;

logic_selector refers to raw logic name;

clarified terminology;

tuned signature;

do not store bulky Session.Deps;

avoid duplicate invocation of expensive Sessions.deps on full_sessions; tuned;

added isabelle jedit options -B, -P, clarified -R; misc tuning and clarification;

no heap sharing for empty session (e.g. HOL-ODE);

tuned diagram;

clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;

removed unused option, which is potentially expensive;

allow to augment session context via explicit session infos; more compact required_session interface;

synthesize session with all required theories from other session imports;

clarified signature;

clarified signature;

clarified signature;

clarified signature;

clarified signature: global_theories is always required;

tuned;

tuned signature;

clarified modules;

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

more permissive: db could be empty after hard crash;

no censorship (in contrast to 2c828c830ad7);

A few more topological results. And made some slow proofs faster

removed ancient nat-int transfer

added lemma

added 'mlex_iff' lemma and simplified proof

merged

recovered document from 9bfb6978eb80;

NEWS;

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;

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;