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;

clarified signature;

relaxed assm

back to build_polyml_component according to 54c6ec4166a4 (amending 808e6ddb5a50);

reactivated unfinished tool (cf. a3a847c4fbdb);

tuned whitespace;

clarified meta_digest;

tuned;

added isablle build option -f;

canonical multiplicative euclidean size

clarified parity

clarified uniqueness criterion for euclidean rings

tuned proofs

tuned imports

fixed markup

ignore isolated nodes by default;

merged

cycle check with informative error;

tuned: each session has at most one defining entry;

more operations;

tuned signature;

tuned signature;

Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems

Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.

merged

tuned: less oo-non-sense;

operations for graph display;

tuned signature;

dependencies of entries vs. sessions; json output like "isabelle afp_dependencies"; misc tuning;

some administrative support for AFP;

tuned;

clarified signature: public access to ROOT file syntax;

euclidean rings need no normalization

more fundamental definition of div and mod on int

one uniform type class for parity structures

generalized some rules

avoid variant of mk_sum

adjusted implementation according to comment

dropped duplicates

generalized simproc

replaced recdef were easy to replace

elementary definition of division on natural numbers

tuned structure

abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

Polynomial_Factorial does not depend on Field_as_Ring as such

avoid name clashes on interpretation of abstract locales