2014-08-10 wenzelm 2014-08-10 merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
2014-08-10 wenzelm 2014-08-10 updated URL (anticipate merge with 85b8cc142384);
2014-08-10 wenzelm 2014-08-10 Added tag Isabelle2014-RC3 for changeset 91e188508bc9
2014-08-10 wenzelm 2014-08-10 proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;
2014-08-10 wenzelm 2014-08-10 follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
2014-08-09 wenzelm 2014-08-09 tuned;
2014-08-09 wenzelm 2014-08-09 tuned;
2014-08-09 wenzelm 2014-08-09 tuned;
2014-08-09 wenzelm 2014-08-09 tuned comments;
2014-08-09 wenzelm 2014-08-09 clarified synchronized scope;
2014-08-09 wenzelm 2014-08-09 tuned comments;
2014-08-08 wenzelm 2014-08-08 application manifest for Windows 8/8.1 dpi scaling;
2014-08-08 wenzelm 2014-08-08 observe context visibility -- less redundant warnings;
2014-08-08 wenzelm 2014-08-08 improved monitor panel;
2014-08-05 wenzelm 2014-08-05 protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");
2014-08-05 wenzelm 2014-08-05 added system option editor_output_delay: lower value might help big sessions under low-memory situations;
2014-08-05 wenzelm 2014-08-05 obsolete (see f7700146678d);
2014-08-05 wenzelm 2014-08-05 tuned proofs -- fewer warnings;
2014-08-05 wenzelm 2014-08-05 clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;
2014-08-05 wenzelm 2014-08-05 avoid duplication of warnings stemming from simp/intro declarations etc.;
2014-08-05 wenzelm 2014-08-05 tuned proofs;
2014-08-05 wenzelm 2014-08-05 restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;
2014-08-05 wenzelm 2014-08-05 tuned;
2014-08-05 wenzelm 2014-08-05 more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
2014-08-05 wenzelm 2014-08-05 refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
2014-08-04 wenzelm 2014-08-04 even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);
2014-08-04 wenzelm 2014-08-04 tuned;
2014-08-04 wenzelm 2014-08-04 tuned;
2014-08-04 wenzelm 2014-08-04 Added tag Isabelle2014-RC2 for changeset ee908fccabc2
2014-08-04 wenzelm 2014-08-04 more user aliases;
2014-08-04 noschinl 2014-08-04 registered Haskabelle-2014
2014-08-01 Lars Noschinski 2014-08-01 tuned, so codegen runs with current isabelle again
2014-08-03 wenzelm 2014-08-03 tuned whitespace;
2014-08-03 wenzelm 2014-08-03 more robust popup geometry vs. formatted margin;
2014-08-03 wenzelm 2014-08-03 tuned message;
2014-08-02 wenzelm 2014-08-02 updated URL;
2014-08-02 wenzelm 2014-08-02 tuned;
2014-08-02 wenzelm 2014-08-02 updated URL;
2014-08-02 wenzelm 2014-08-02 more emphatic warning via error_message (violating historic TTY protocol);
2014-08-02 wenzelm 2014-08-02 proper priority for error over warning also for node_status (see 9c5220e05e04);
2014-08-02 wenzelm 2014-08-02 more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
2014-08-02 wenzelm 2014-08-02 always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;
2014-08-02 wenzelm 2014-08-02 tuned output;
2014-08-01 wenzelm 2014-08-01 prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
2014-08-01 blanchet 2014-08-01 careful when calling 'Thm.proof_body_of' -- it can throw exceptions
2014-08-01 wenzelm 2014-08-01 removed unused stuff;
2014-08-01 wenzelm 2014-08-01 agree on keyword categories with ML;
2014-08-01 wenzelm 2014-08-01 more keyword categories (as in ML);
2014-07-31 wenzelm 2014-07-31 prefer dynamic ML_print_depth if context happens to be available;
2014-07-31 wenzelm 2014-07-31 completion popup supports both ENTER and TAB (default);
2014-07-31 wenzelm 2014-07-31 clarified compile-time use of ML_print_depth;
2014-07-31 wenzelm 2014-07-31 more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
2014-07-30 blanchet 2014-07-30 correctly resolve selector names in default value equations
2014-07-30 kuncar 2014-07-30 update documentation for Lifting/Transfer
2014-07-30 kuncar 2014-07-30 add Isabelle Datatype Manual to the bibliography
2014-07-30 wenzelm 2014-07-30 CONTRIBUTORS;
2014-07-30 kuncar 2014-07-30 NEWS
2014-07-29 hoelzl 2014-07-29 better ordering of positive_integral renaming to nn_integral in NEWS
2014-07-28 desharna 2014-07-28 made tactic more robust w.r.t. dead variables; tuned;
2014-07-27 blanchet 2014-07-27 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly