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;

tuned comment;

more explicit bootstrap_thy; clarified error;

explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;

clarified thy_deps;

tuned;

tuned signature;

misc tuning and clarification;

let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);

rewrite: use distinct names for unnamed abstractions

avoid mix of languages;

merged

NEWS;

ensure that deps are defined in entries, to prevent crash of Graph_View.build_graph;

updated to jdk-7u80, the latest and last public release of Java 7;

session graph with folded base theories, as in document preparation;

tuned signature;

merged

rewrite: add ML interface

use wasysym for \<hole>;

tuned signature, clarified modules;

tuned messages;

obsolete (see also 94b2690ad494);

GUI controls for ML_statistics, for more digestible protocol dump;

more robust error handling of commands that are declared but not yet defined;

NEWS;

clarified sledgehammer options to approximate old-style diagnostic command;

prepared for more meta-simp rules (by Stefan Berghofer)

merged

add various lemmas about pmfs

lemmas about integrals over bind and join on measures

add lemmas

generalise lemmas; add version of monotone convergence for countable integrals

add lemma about monotone convergence for countable integrals over arbitrary sequences

add lemmas about restrict_space

move lemma from AFP/Coinductive

move some lemmas from AFP/Coinductive

more lemmas about ereal

more lemmas for cset

add lemmas

add lemmas

merged

rewrite: tuned code, no semantic changes

rewrite: with asm pattern, propagate also remaining assumptions to new subgoals

rewrite: do not descend into conclusion of premise with asm pattern

rewrite: with asm pattern, try all premises for rewriting, not only the first

tuned

rewrite: propagate premises to new subgoals

reformat comments

rewr_cconv: ignore premises when tuning conclusion

enable \<hole> syntax for rewrite

call Goal.prove only once for a quadratic number of theorems

predicate compiler: ignore Abs_filter and Rep_filter

merged

moved _aux functions from AFP/Collections to AList

merged

replace Filters in NSA by HOL-Filters

move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter

add cofinite filter

add frequently as dual for eventually

add quantifier syntax for eventually

move filters to their own theory

fix latex in Transcendental

proper site for Cygwin setup;

less ambitious collection of quasi-generic PIDE modules;

tuned;

autorebase.bat.done no longer exists in Cygwin 1.7.35 -- lets hope that its incremental rebasing works for us;

merged

tuned -- avoid ML warnings;

avoid redundant shell process;

clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;

Restored LIMSEQ_def as legacy binding. [The other changes are whitespace only.]

tuned;

merged

proper Pretty.brk -- redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);

tuned whitespace;

Merge

Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.

Merge

Merge

Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.

updated for release;

updated for release;

Added tag Isabelle2015-RC0 for changeset 42d34eeb283c