tuned message;

separate syslog dockable -- discontinued tendency of sub-window management via tabs;

clarified prover startup: no timeout, read stderr more carefully;

need to close_input before expecting threads to terminate/join; tuned signature;

make double sure that GUI components are up-to-date after init;

tuned message;

more explicit treatment of return code vs. session phase;

tuned signature;

separate README dockable, which allows to make it more prominent first and remove it later;

added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS

shortened yet more multiset proofs; added lemma size_multiset_of [simp]

remove unused intermediate lemma

shortened more multiset proofs

shortened some proofs

use transfer method for instance proof

tweaked remote Vampire setup

update docs

killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8

don't generate definitions for LEO-II -- this cuases more harm than good

dropped sort constraints on datatype specifications

potentially more convincing kill -TERM of feeder (cf. 32c03d45fffe) -- attempt to workaround spurious perl "hangs" on lxbroy10;

tuned proofs;

further attempts to simplify/robustify Swing_Thread.now, to avoid spurious physical race conditions on Java 6 / Mac OS X;

ignore empty messages even on tty, e.g. relevant for Isabelle_System.bash_output err output;

discontinued obsolete Cygwin module;

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

generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command

infrastructure that makes possible to prove that a relation is reflexive

temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)

lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up

treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect

get ready for automatic generation of extensionality helpers

minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)

more helpful error message

transfer rules for many more list constants

made SML/NJ happy

repair the Waldmeister endgame only for Waldmeister proofs

fixed Waldmeister commutativity hack

imported patch atp_tuning

add transfer rules for nat_rec and funpow

add transfer rule for constant List.lists

add transfer rule for set_rel

ensure the "show" equation is not reoriented by Waldmeister

ensure consistent naming of Waldmeister proof steps, so that they are not cleaned away by "clean_up_atp_proof_dependencies"

repaired snag in debug function

graceful handling of Waldmeister endgame

improve parsing of Waldmeister dependencies (and kill obsolete hack)

tuning

added debugging function

LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover

eta-reduce definition-like equations for THF provers; Satallax in particular seems to love that

get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default

extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps"

reintroduced example now that it's no longer broken

fixed "real" after they were redefined as a 'quotient_type'

temporarily comment out broken nitpick example; adapt to new definition of type rat

simplify instance proofs for rat

convert Rat.thy to use lift_definition/transfer

cleaner handling of bi-implication for THF output of first-order type encodings

distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers

temporarily comment out broken nitpick example