more NEWS/CONTRIBUTORS;

improved editing support for control styles; separate module for Isabelle actions;

added ISABELLE_PLATFORM_FAMILY;

merged

moved lemma

timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);

add quotient_of_div

generate correct names

simplified code

generate correct correspondence relation name

more uniform title, follow-up to 928cb8b35e6e;

tuned

defer interpretation of markup via implicit print mode;

merged

made SML/NJ happier

pack window before accessing its geometry;

always refresh font metrics, to help window size calculation (amending 2585c81d840a);

more precise tooltip window size;

take component width as indication if it is already visible/layed-out, to avoid multiple formatting with minimal margin;

reset active area for outdated snapshot (again?);

some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;

more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;

some support for breakable text and paragraphs; tuned Symbol.scanner, which operates on symbols, not characters;

tuned names

tuned comment;

clarified symbol groups, despite this traditional arrangement in X-symbol grid;

always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;

tuned whitespace;

merged

included abbrev in tooltip

removed (unicode) tooltips: can not adjust font in basic swing tooltip

delayed search to improve reactivity

respect font property for symbols

capitalize lowercase groups; tuned with mkString

merged

more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML; more generous timeout for HOL-Quickcheck_Examples, which is rather slow in checking its examples (and mostly sequential);

Countable_Set: tuned lemma names; more generic lemmas

enable Symbols dockable by default;

tuned;

accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;

renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set

dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; search field for symbols

CONTRIBUTION: add fabians work

NEWS: document changes in HOL-Probability

NEWS (changeset 13211e07d931): add Countable_Set

NEWS (changeset 69b35a75caf3): document changes in FuncSet

new theory of immutable arrays

some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;

support for symbol groups, retaining original order of declarations; updated WWW_Find: untested change of ad-hoc parser of ~~/etc/symbols;

tuned;

add Countable_Set theory

tuned proof

simplified command line of "isabelle install";

known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);

some documentation for "algebra" in HOL;

global default for session timeout;

alternative completion for outer syntax keywords;

init options on startup as well;

theorem status about oracles/futures is no longer printed by default; renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;

tuned: use induction rule sigma_sets_induct_disjoint

tuned FinMap

merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

more refs;

isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release); always generate sty files, as before c5d0f19ef7cb;

proper jvmpath for windows;

more generous tracing_limit, with explicit system option;

adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;

update options via protocol; jEdit dialog for "Parallel Checking" options;

more accurate pixel_range -- do not round offset here;

tuned signature;

prefer absolute default $USER_HOME/Scratch.thy;

more portable process exit;

tuned -- eliminate pointless ML method definition;

tuned;

NEWS;

tuned structure of Isabelle/HOL;

method setup for Classical steps;

tuned signature;

updated keywords;

moved (b)choice_iff(') to Hilbert_Choice

move theorems to be more generally useable

merged

made SML/NJ happy;

renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space

renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose

measurability for nat_case and comb_seq

rules for AE and prob

rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication

more measurability rules

renamed to more appropriate lim_P for projective limit

allow arbitrary enumerations of basis in locale for generation of borel sets

repaired slip accidentally introduced in 57209cfbf16b

prefer implementation in HOL; n.b. code_reflect cannot reflect type synonyms

corrected headers

hide constants of auxiliary type finmap

generalized to copy of countable types instead of instantiation of nat for discrete topology

added projective limit; proof is based on auxiliary type finmap::polish_space

regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards

tuned -- eliminated obsolete citation of isabelle-ref;

updated basic equality rules;

removed somewhat pointless historic material;

updated unification options;

removed some historic material that is obsolete or rarely used;

tuned;

updated section on ordered rewriting;

updated subgoaler/solver/looper;

removed somewhat pointless historic material; tuned;

tuned;

updated explanation of rewrite rules;

(re)moved old material about Simplifier;

some coverage of "resolution without lifting", which should be normally avoided;

removed somewhat pointless historic material;

updated biresolve_tac, bimatch_tac; removed obscure historical material;

moved classical wrappers to IsarRef; removed somewhat pointless historic material;

avoid clash of terminology wrt. "semi-automated" in the sense of Isar (e.g. method "rule");

updated citations;

tuned;

removed junk;

removed pointless historic material;

more on Simplifier rules, based on old material;