more precise handling of java failure, due to missing ISABELLE_JDK_HOME;

tuned some proofs; removed duplicate lemma zero_le_imp_of_nat

centralized enriched_type declaration, thanks to in-situ available Isar commands

tuned whitespace

replace locale 'UFT' with new un-named context block feature; use locale begin/end instead of 'in';

more CONTRIBUTORS;

some coverage of bundled declarations;

more uniform outline;

some coverage of unnamed contexts, which can be nested within other targets;

gathered mirabelle_sledgehammer's hardcoded defaults

Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action

Mirabelle now gives usage info when no arguments given

switched from using sed to perl in mirabelle tool

renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;

refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"; clarified thin_prems_tac: fail as tactic without error;

merged;

removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example

aligned tptp_graph dependencies to Isabelle conventions;

more ambitious isatest settings using polyml-svn (e.g. 1487);

use official TextArea.isCaretVisible and thus follow the "blink" flag; updated jedit_build component;

display more memory;

keyword ";" is declared via prover (as "minor", not "diag");

outermost SELECT_GOAL potentially improves performance;

report ISABELLE_HOME_WINDOWS;

chmod +x;

more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;

misc tuning for release;

revert changes of already published NEWS;