clarified old forms;

Added tag Isabelle2016-RC4 for changeset f4baefee5776

tuned proofs;

more on Mac OS X with Retina display;

re-init document views for the sake of Text_Overview size;

removed unused cancel operation;

separate delay_repaint to ensure reactivity, indepently of future_refresh status; clarified delay_refresh: do not cancel already running task, but retry later;

suppress ISABELLE_ROOT after init, to avoid conflict with ISABELLE_HOME when folding file names in "isabelle jedit" command-line tool;

clarified;

recovered handle_resize from 5922db0430f1;

preplaying of 'smt' and 'metis' more in sync with actual method

updated HOL-specific section w.r.t. datatypes

proper markup for formal text;

Added tag Isabelle2016-RC3 for changeset 81cbea2babd9

tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;

more on "ML debugging within the Prover IDE";

updated to official polyml-5.6;

misc tuning and updates;

misc tuning and updates;

misc tuning;

allow single quote within URL;

proper try_run for exactly one evaluation of body (amending 91c3aedbfc5e);

more thorough syntax_changed: new commands need require new folds;

Added tag Isabelle2016-RC2 for changeset 5d513565749e

proper nesting: 'qed' needs to close the corresponding 'proof' and goal statement;

clarified exception handling;

guard sessions that no longer work with SML/NJ -- memory problems;

tuned signature; tuned;

tuned;

tuned;

tuned;

proper NEWS for this release;

more CONTRIBUTORS;

tuned;

discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;

back to elementary options used in Isabelle2015 for jdk-7 -- none of the intermediate experiments for jdk-8 improved reactivity on particular dual-CPU system, but the problem seems to be absent on common single-CPU systems;

empty abbrevs are removed globally;

tuned markup, e.g. relevant for Rendering.tooltip;

tuned message;

more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized;

report error on internal channel as well: startup_failure dialog may be too late;

clarified errors: more explicit treatment of uninitialized state;

check more files;

updated header;

tuned text

tuned

synchronized with book

tuned

avoid error in Isar proof reconstruction if no ATP proof is available

preplaying of 'smt' and 'metis' more in sync with actual method

avoid generating polymorphic SPASS constructs to monomorphic SPASS

Reorganised a huge proof

back to post-release mode -- after fork point;

merged

bypass input method for better imitation of read-only mode (cf. f26a4d5e82b5): e.g. relevant for composition of ALT-u u on Mac OS X;

tuned;

clarified -- this is available on Mac OS X, too;

updated jdk;

tuned signature (according to Scala version);

fixed NEWS w.r.t. multisets

added 'supset' variants for new '<#' etc. symbols on multisets

added lemma

tuned;

tuned;

tuned

merged

added lemma

Added approximation of powr to NEWS/CONTRIBUTORS

Made Approximation work for powr again

updated polyml;

tuned whitespace;

updated mirrors according to website;

renamed map_of to lookup

more method definitions;

tuned syntax;

tuned;

misc tuning and modernization;

keep src/Doc;

tuned URLs according to website;

more symbols;

tuned message;

tuned message;

Added tag Isabelle2016-RC1 for changeset 155d30f721dd

misc updates and tuning; more on "Output" versus "Proof state";

misc updates and tuning;

misc updates and tuning;

continuity of parameterized integral; easier-to-apply formulation of rules

tuned;

tuned;

tuned;

made SML/NJ happy;

removed dead code;

tuned syntax;

isabelle update_cartouches -c -t;

eliminated spurious Unicode;

clarified example;

updated section on "Overloaded constant definitions";

more doc content;

tuned;

removed old 'defs' command;

Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;

more doc content;

merged;

tuned signature;

proper relative symlink;

tuned;

Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);

merged

tuned layout

updated NEWS

generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes

more good NEWS;

misc tuning and modernization;

merged

updated old screenshots, added new screenshots;

more explicit errors for control symbols that are left-over after Markdown parsing;

removed in anticipation of c92d82c3f41b -- demolition after renovation;

eliminated old defs;

eliminated old defs;

clarified axiomatization versus definitions; eliminated old defs; more symbols;