eliminated unused Cygwin download;

simplified Cygwin root: warm start via env, cold start via property, no registry magic;

include scala-compiler.jar in basic Isabelle/Scala environment, to make Isabelle/jEdit console work with scala-2.10.0-M3;

tuned proofs;

less warning in scala-2.10.0-M3;

avoid scala.tools.nsc.Interpreter -- deprecated in scala-2.9.0; discontinued support for scala-2.8.x;

make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)

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;

tuned proof;

prefer symbolic "contrib" -- mira should have a symlink to physical contrib_devel;

merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;

compile

don't apply "ext_cong_neq" to biimplications

added one slice with configurable simplification turned off

make higher-order goals more first-order via extensionality

added "ext_cong_neq" lemma (not used yet); tuning

use quot_del instead of ML code in Rat.thy

quot_del attribute, it allows us to deregister quotient types

invite users to upgrade their SPASS (so we can get rid of old code)

start phasing out old SPASS

minor tweak in Vampire setup

include "ext" in all Satallax proofs

add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"

tuning

added helper -- cf. SET616^5

note Quotient theorem for typedefs in setup_lifting

added a timeout to "try0" in Mirabelle

don't generate code in Word because it breaks the current code setup

robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)

added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)

remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now