more uniform usage of "isabelle tool";

less verbosity;

proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;

tuned signature;

updated ROOT according to 3defa60a7ae3;

merged

re-activating Quickcheck_Narrowing_Examples in Quickcheck_Examples

added build option -c; tuned;

removed build option -f (cf. a125b8040ada), due to slightly inconvenient behaviour on ancestors;

script for downloading components from central store

added build option -f;

corrected slip

discontinued $ISABELLE_HOME/build (cf. 500c6eb6c6dc);

separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;

added Quickcheck_Benchmark (cf. 1959baa22632);

no apparent need for single-threaded execution;

discontinued obsolete Isabelle/build script;

announce advanced support for Isabelle sessions and build management;

some introduction on sessions;

tuned messages;

tuned;

added generated file;

some description of main build options;

more on "Session ROOT specifications";

some description of isabelle build;

tuned;

isabelle browser is another user interface;

renamed isabelle-root minor mode;

discontinued special treatment of Proof General;

top-down order of user interfaces;

misc tuning;

move exception handlers outside of let block

tuned message;

merged

evaluation: allow multiple code modules

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

merged

restored narrowing quickcheck after 6efff142bb54

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used

replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms

give Nat_Arith simprocs proper name bindings by using simproc_setup

tweaks in preparation for type encoding evaluation

merged

replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones

nicer Nitpick subscript output in jEdit

no_check for @{setting} antiquotations -- empty values are treated as undefined on Cygwin;

proper shell variable;

actually check return code;

include doc-src as component, and thus its sessions defined in ROOT;

tuned signature;

delete other log file;

simplified Path vs. JVM File operations;

tuned;

tuned messages;

fewer options;

tuned signature;

prefer explicit datatype Present.dump_mode;