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;

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