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;