add reference

merged

add BNF instance for Dlist

crediting LCP in CONTRIBUTORS

more careful witness' type analysis

removed outdated example

remove unused code

remove Eisbach's dependency on HOL

match method now makes proper use of context_tactic

merged

nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.

added AA_Map; tuned titles

tuned

Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.

generalized proofs

avoid generating TFF1 or polymorphic DFG constructs in Vampire or SPASS problems for goals containing schematic type variables

tuning

exported ML function

setup code generation for filters as suggested by Florian

merged

filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones

isar-ref entry for print_record

add more frequently-run test for print_record

print_record NEWS and CONTRIBUTORS

print_record: diagnostic printing of record definitions

misc tuning and modernization;

prune old versions more often, to reduce overall heap requirements;

generate HTML version of NEWS, with proper symbol rendering;

tuned -- according to ML version;

suppress somewhat pointless description (NB: this is displayed in 'print_methods');

merged

tuned syntax;

tuned;

\<struct> loses its rendering and is superseded by \<diamondop>; tuned;

discontinued \<struct> syntax;

tuned whitespace;

tuned;

clarified symbol insertion, depending on buffer encoding;

tuned;

fix code generation for uniformity: uniformity is a non-computable pure data.

add uniform spaces

merged

merged

tuned;

merged

more uniform treatment of symblinks: avoid confusion when unpacking .tar.gz bundle with NTFS links;

tuned signature;

prefer non-ASCII output;

more uniform treatment of package internals;

more thorough GUI update;

tuned;

added lemma

Tuned constant approximations

merged

revisions to limits and derivatives, plus new lemmas

Added formal power series updates to NEWS/CONTRIBUTORS

Tuned approximations in Multivariate_Analysis

misc tuning for release;

add the proof of the central limit theorem

nicer 'Spec_Rules' for size function

updated docs

updated NEWS

more complete setup for 'Rat' in Nitpick

more systematic treatment of dynamic facts, when forming closure;

clarified ROOT files;

proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;

added ML antiquotation @{method};

tuned;

tuned;

isabelle update_cartouches -c -t;

merged

more realistic Eisbach method invocation from ML; misc tuning and clarification;

unused;

more robust event propagation;

Fixed sectioning in HOL/Library/Polynomial

Merged

Added some facts about polynomials

misc tuning for release;

merged

fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;

tuned;

Added summability/Gamma/etc. to NEWS and CONTRIBUTORS

proper latex setup;

updated headers;

merged

ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;

Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)

merged

tuned proofs;

node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;

stop dummy sessions as well;

clarified order of shutdown;

Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function

retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);

proper treatment of RAW bootstrap session;

tuned whitespace;

more symbols; tuned;

tuned spacing of \<partial>; spontaneous update of .sfd files due to fontforge;

eliminated somewhat pointless and obscure options;

isabelle update_cartouches -c -t;

tuned;

proper platform_path for Windows;

clarified isabelle jedit command-line;

tuned;

avoid downloading contrib again;

provide server name uniformly on all platforms;

more symbols;

NEWS;

keep platform bundle for reference, e.g. for headless installation;

keep generic archive for all platforms -- required for Admin/Release/build_library;

oops;

Added tag Isabelle2016-RC0 for changeset e18444532fce

tuned;

updated for release;

tuned;

more symbols;

clarified abbrev;

clarified meaning of \<^bold> action, depending on group;

clarified groups, notably for Symbols dockable;

glyphs for \<bind>, \<then>;