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