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;

eliminated old defs;

eliminated old defs;

eliminated old defs;

eliminated old defs;

eliminated old defs;

eliminated old defs;

Deleted problematic code equation in Binomial temporarily.

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)