clarified synchronized scope;

tuned comments;

application manifest for Windows 8/8.1 dpi scaling;

observe context visibility -- less redundant warnings;

improved monitor panel;

protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");

added system option editor_output_delay: lower value might help big sessions under low-memory situations;

obsolete (see f7700146678d);

tuned proofs -- fewer warnings;

clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;

avoid duplication of warnings stemming from simp/intro declarations etc.;

tuned proofs;

restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;

tuned;

more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;

refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;

even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);

tuned;

tuned;

Added tag Isabelle2014-RC2 for changeset ee908fccabc2

more user aliases;

registered Haskabelle-2014

tuned, so codegen runs with current isabelle again

tuned whitespace;

more robust popup geometry vs. formatted margin;

tuned message;

updated URL;

tuned;

updated URL;

more emphatic warning via error_message (violating historic TTY protocol);

proper priority for error over warning also for node_status (see 9c5220e05e04);

more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);

always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;

tuned output;

prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);

careful when calling 'Thm.proof_body_of' -- it can throw exceptions

removed unused stuff;

agree on keyword categories with ML;

more keyword categories (as in ML);

prefer dynamic ML_print_depth if context happens to be available;

completion popup supports both ENTER and TAB (default);

clarified compile-time use of ML_print_depth;

more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;

correctly resolve selector names in default value equations

update documentation for Lifting/Transfer

add Isabelle Datatype Manual to the bibliography

CONTRIBUTORS;

NEWS

better ordering of positive_integral renaming to nn_integral in NEWS

made tactic more robust w.r.t. dead variables; tuned;

do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly

some actual workaround to remove document nodes;

Added tag Isabelle2014-RC1 for changeset c0fd03d13d28

tuned;

tuned

add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations

tuned

no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property

generate nicer 'set' theorems for (co)datatypes

compile

took out test driver

make TPTP tools work on polymorphic (TFF1) problems as well

put comments between TPTP lines to comply with TPTP BNF

test driver

treat variables as frees in 'conjecture's

support TFF1 in TPTP parser/interpreter

tuning

tuned

tuned

tuned

merged

handle deep nesting in N2M

made tactic more robust

added lemma

replaced misleading - by _

more correct clique computation for N2M

regenerated ML-Lex/Yacc files

correctly interpret arithmetic types

added 'datatype_compat' tests

tuning whitespace

tuned skolemization

rationalize Skolem names

tuning

tuned code

don't rename variables which will be renamed later anyway

normalize skolem argument variable names so that they coincide when taking the conjunction

tuning

tuned comments

deal with E definitions

updated 'compress' docs

cleaner 'compress' option

renamed 'sh_minimize' to 'minimize'; compile;

restored more sorting

tuned terminology (cf. 'isar_proofs' option)

sort facts in minimizer as well

default on 'metis' for ATPs if preplaying is disabled