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;