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;

merged

completion supports theory header imports; tuned;

clarified modules;

tuned signature;

new theorem at_within_cbox_finite

process ROOT files only once, which allows duplicate (or overlapping) session root directories;

prefer Cygwin64, although some components still require update;