adding abstraction layer; more precise function names

adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used

determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations

only annotating constants with sort constraints

also adding type annotations for the dynamic invocation

removed legacy lemmas in Complete_Lattices

increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling

more isatest stats;

refined Symbol.is_symbolic -- cover recoded versions as well;

double clicks switch to document node buffer;

tuned;

explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);

at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;

instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);

unique file names via serial numbers, to allow files like "root" or multiple files with same base name;

imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;

merged

numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else

removed obsolete patches for PG 4.1;

additional space for borderless UI;

more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);

explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;

isatest settings for macbroy6 (Mac OS X Lion);

more Mac OS reference hardware;

updated to SML/NJ 110.73;

tentative announcement based on current NEWS;

tuned;

separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);

updated for release;

tuned;