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

convert real number theory to use lifting/transfer

tuned ordering of lemmas

pass fewer facts to LEO-II and Satallax

tweak LEO-II setup

use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)

build Pure_64 with new settings

tuned

playing around with mira settings

defining and proving Executable_Relation with lift_definition and transfer

specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

prevent spurious timeouts

added "try0" tool to Mirabelle

use latest E (1.5)

lifting package produces abs_eq_iff rules for total quotients

using the new transfer method to obtain abstract properties of RBT trees

back to post-release mode -- after fork point;

removed obsolete RC tags;

Added tag Isabelle2012 for changeset 21c42b095c84

try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

Added tag Isabelle2012-RC3 for changeset ed5f56b8f90a

some message;

tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;

Fixed disambiguation of names (cf. 5759ecd5c905)

merged

file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation;

prefer absolute paths, to allow launching from a different context (e.g. via file associations);

tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";

allow spaces in target directory;