integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)

added FIXMEs

Replaced { } proofs by local lemmas; added Hoare logic with logical variables.

backed out odd "bug fix" 671decd2e627;

more recent polyml-test version; afford more heap by default: all platforms are now 64bit and presumably have sufficient memory;

minimal document model for theory files;

tuned signature;

tuned signature;

more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);

uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");

updated comments;

updated to scala-2.12.4;

testing NewTestRegisterSave;

superseded by plain_identify;

tolerate odd negative times from old log files (before 1698e9ccef2d);

prefer main entry points of HOL;

tuned signature;

clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;

more robust sorted_entries;

more convenient build_log_history;

tuned;

more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;

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;