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

avoid trivial definition

canonical introduction and destruction rules for pairwise

avoid fact name clashes

spelling and tuned whitespace

tuned

fundamental property of division by units

removed mere toy example from library

tuned proofs

dropped dead code

Fixed the theorem name "closed_imp_fip_compact"

new material about connectedness, etc.

more on Docker;

removed obsolete RC tags;

build_docker is regular tool (non-admin);

merged

Added tag Isabelle2017 for changeset 64b47495676d

obsolete;

more NEWS;

updated for release;

merged

proper File.platform_path for SML/NJ on Windows;

clarified signature;

proper output of raw ML;

theory qualifier is always session name (see also 31e8a86971a8);

clarified session structure;

discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;

merged

clarified empty merge; tuned;

permissive loaded_theories (amending 67dbf5cdc056): user errors are produced e.g. in Known.make;

prefer native platform x86-windows, to make this work on x86_64-cygwin;

tuned signature;

even more robust syntax (amending 122df1fde073);

clarified error for bad session-qualified imports;

clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;