clarified signature;

clarified signature;

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

ran isabelle update_op on all sources

discontinued obsolete print mode;

avoid 'hence' and 'thus' in generated proofs

renamed "pairself" to "apply2", in accordance to @{apply 2};

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

make sure no '__' suffixes make it until Isar proof

rename skolem symbols in the negative case as well

use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)

generate 'thesis' variable in Sledgehammer Isar proofs

three-line 'obtain' format for generated Isar proofs

reintroduced two-line-per-inference Isar proof format

tuned skolemization

rationalize Skolem names

rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures

more robustness in Isar proof construction

introduce fact chaining also under first step

better handling of variable names

nicer generated variable names

given two one-liners, only show the best of the two

don't generate Isar proof skeleton for what amounts to a one-line proof

basic setup for zipperposition prover

correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs

use 'simp add:' syntax in Sledgehammer rather than 'using'

integrate SMT2 with Sledgehammer

don't lose additional outcomes

generate comments in Isar proofs

refactor relabeling code

tuned data structure

tuned data structure

more flexible compression, choosing whichever proof method works

renamed ML file

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

merged 'reconstructors' and 'proof methods'

added 'smt' as a proof method

tuning

more data structure rationalization

rationalized threading of 'metis' arguments

simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods

generalized preplaying infrastructure to store various results for various methods

added a 'trace' option

moved code around

added 'algebra' to the mix

more informative trace

tuning

more concise Isar output

better tracing + syntactically correct 'metis' calls

tuned ML function names

tuning

moved ML code around

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