removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)

isabelle update -u control_cartouches;

added option for noncommercial Vampire

uniform use of Standard ML op-infix -- eliminated warnings;

ran isabelle update_op on all sources

made MaSh faster and less likely to hang seemingly forever

killed final stops in Sledgehammer and friends

clarified syntax categories;

eliminated "xname" and variants;

tuned signature;

create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);

further reduced dependency on legacy async thread manager

removed legacy asynchronous mode in Sledgehammer

clarified markup;
tuned signature;

keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked)

improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);

put E before (typically remote, hence less reliable) Vampire

silence 'try'

made Auto Sledgehammer behave more like the real thing

sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;

more standard command setup;

explicit error for Toplevel.proof_of;
eliminated obsolete Toplevel.unknown_proof;
more total Toplevel.proof_position_of;

reorder provers to reflect current eval results

@{command_spec} is superseded by @{command_keyword};

tuned default provers

added checkbox for try0;

allow diagnostic proof commands with skip_proofs;

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

discontinued Proof General;

proper syntax categery "name" -- as usual and as documented;

gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)

going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.

tuned signature -- define some elementary operations earlier;

cleaner 'compress' option

reordered provers

compile

eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)

simplified minimization logic

always minimize Sledgehammer results by default

reduced preplay timeout to 1 s

move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects

more generous formula -- there are lots of duplicates out there

automatically learn MaSh facts also in 'blocking' mode

renamed Sledgehammer options

took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale

removed '_new' sufffix in SMT2 solver names (in some cases)

removed old SMT module from Sledgehammer

basic setup for zipperposition prover

silence methods even better

new approach to silence proof methods, to avoid weird theory/context mismatches

improved whitelist (cf. be1874de8344)

more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);

more uniform ML/document antiquotations;

support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;

integrate SMT2 with Sledgehammer

restored old 'remotify' logic -- too many bugs were introduced when refactoring the code

do the right thing with provers that exist only remotely (e.g. e_sine)

renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover

reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense

added 'smt' option to control generation of 'by smt' proofs

tuning

refactor large ML file

renamed many Sledgehammer ML files to clarify structure

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_run.ML => src/HOL/Tools/Sledgehammer/sledgehammer.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_print.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

renamed ML file

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

tuned ML file name

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML