added pred_def, rel_eq_onp tuned

misc tuning, based on warnings by IntelliJ IDEA;

tuned;

updated screenshot;

clarified markup range;

modifier markup for all parsed tokens; report literal token markup, before re-assignment;

updated screenshots;

updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;

avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);

allow sorts on dead variables in BNFs

tuned whitespace;

avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;

code equations as displayable content in code dependency graph

filtering of reflexive dependencies avoids problems with state-of-the-art graph browser; clarified

added checkbox for try0;

made CVC4 support work also without unsat cores

more paranoia settings, e.g. relevant for Ubuntu 15.04;

Added tag Isabelle2015-RC2 for changeset 8483c2883c8c

always traverse required nodes, e.g. relevant for inlined errors of imported theory header;

tuned;

tuned message, in accordance to ML side;

tuned settings to avoid sporadic crashes;

clarified settings for default Poly/ML version: test the actual Isabelle component;

avoid binding warning in Nitpick

doc

clarified permissions;

allow diagnostic proof commands with skip_proofs;

tuned signature;

updated polyml according to fixes-5.5.2 SVN version 2009;

declare Nitpick atoms to avoid '??.' prefixes in output

proper isatest machine;

prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;

this warning is hardly useful but produces noisy markers in the jedit interface

undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)

generalized tends over powr; added DERIV rule for powr

added acknowledgment

general Taylor series expansion with integral remainder

generalized class constraints

generalized differentiable_bound; some further variations of differentiable_bound

moved basic lemmas about has_vector_derivative

closures of intervals

add lfp/gfp rule for nn_integral

strengthened lfp_ordinal_induct; added dual gfp variant

add rules for least/greatest fixed point calculus

rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity

no more simp_legacy_precond

no longer needed

swap False to the right in assumptions to be eliminated at the right end

merged

simplified statement and proof

tuned spelling;

Merge

Merge

Merge

tidying some messy proofs

new simp rule

more formal source, more PIDE markup;

tuned -- avoid odd rebinding of "ctxt" and "context";

tuned;

use smaller example that fits into 64MB string limit of Poly/ML x86 platform;

tuned;

Tidying. Improved simplification for numerals, esp in exponents.

allow sorts on dead variables in BNFs

added known bug

tuning

undid 6d7b7a037e8d

New material about complex transcendental functions (especially Ln, Arg) and polynomials

Fixed a non-terminating proof (almost certainly caused by no change of mind)

new lemma

new ==> simp rule

improved docs

merged

merged

added simp rules for ==>

fixes for limits

New material, mostly about limits. Consolidation.

be less specific about POLYML_HOME, take component setup instead

declare Nitpick atoms to avoid '??.' prefixes in output

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

acknowledgment

suppressed warnings

updated docs, esp. relating to 'datatype_compat'

typo

clarified keywords for quasi-command spans and Sidekick structure;

merged

tuned;

clarified syntax diagram: 'obtains' does not allow prop_pat (although it could and should at some point);

tweak afp mac options, try 64bit

compactified proposition

merged

Added tag Isabelle2015-RC1 for changeset c9760373aa0f

tuned spelling;

sorted by automatic regeneration;

updated polyml according to fixes-5.5.2 SVN version 2007;

make SML/NJ happy;

just one line, to make it work with makedist_bundle;

merged

added Eisbach, using version 3752768caa17 of its Bitbucket repository;

merged

rewrite: work purely conversion-based

ANNOUNCE material, based on NEWS;

tuned;

tuned for release;

merged;

finprod takes 1 in case of infinite sets => remove several "finite A" assumptions

(low importance) NEWS

merged

merged

rewrite: add default pattern "in concl" for more cases

more session groups;

allow to exclude session groups;

merged

removed trivial lemmas

proper Theory.check;

make SML/NJ happy;

merged;

clarified document antiquotation: same check as in ML antiquotation;

formal Theory.check, with markup and completion;

tuned;

discontinued pointless warnings: commands are only defined inside a theory context;