fixed soundness bug in Nitpick related to unfolding -- the unfolding criterion must at least as strict when looking at a definitional axiom as elsewhere, otherwise we end up unfolding a constant's definition in its own definition, yielding a trivial equality

more robust Swing_Thread.now: allow body to fail;

tuned proofs;

reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");

merged

update Satallax setup based on evaluation

merged

drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems

prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

gracefully handle definition-looking premises

simplified Poly/ML setup -- 5.3.0 is now the common base-line;

discontinued support for Poly/ML 5.2.1;

less specific sample usage;

some post-release notes;

tuned names

order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)

improved LEO-II definition handling -- still hoping for a fix directly in LEO-II

augment Satallax unsat cores with all definitions

better handling of incomplete TSTP proofs

generate THF definitions

build hybrid Isabelle component for JDK on x86-linux/x86_64-linux;

merged

eliminated old 'axioms';

discontinued obsolete method fastsimp / tactic fast_simp_tac;

eliminated obsolete fastsimp;

extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0

merged

doc updates

lower the monomorphization thresholds for less scalable provers

more explicit proof; misc tuning;