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;

some updates for release;

more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;

updated Scala/JVM versions;

include trailing comments in proper_command range;

minimal support for x86-mingw;

recognize MacOS on modern Java implementations, notably OpenJDK 1.7;

updated to Scala 2.9.2;

updated headers;

eliminated hard tabs;

Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

NEWS

adapt to changes in RBT_Impl

move RBT implementation into type class contexts

misc tuning; atbroy100 no longer available (?);

NEWS

merged

distributivity of * over Un and UNION

Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *

removed "setsum_set", now subsumed by generic setsum

backported Set_Algebras to use type classes (basically reverting b3e8d5ec721d from 2008)

tuned README;

direct scala toplevel tools to ISABELLE_JDK_HOME;

simplified component structure;

merged

merged

generalise case certificates to allow ignored parameters

merged

manual merge

dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"

renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")

more standard method setup;

more precise declaration of goal_tfrees in forked proof state;

partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;

multiset operations are defined with lift_definitions; tuned proofs;

remove outdated comment

rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;

standardized ML aliases;

clarified proof_result: finish proof formally via head tr, not end_tr;

tuned;

more robust Future.fulfill wrt. duplicate assignment and interrupt;

tuned message;

always signal after cancel_group: passive tasks may have become active;

just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update; explicit terminate_execution; tuned source structure;

merged

moved lift_raw_const wrapper out of the Quotient-package into Nominal2