clarified signature;

tuned: prefer list operations over Source.source;

discontinued obsolete print mode;

tuned signature -- more abstract type thm_node;

discontinued raw symbols;
discontinued Symbol.source;
use initial Symbol.explode;

killed final stops in Sledgehammer and friends

eliminated "xname" and variants;

prefer infix operations;

removed too aggressive underscorization

further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes

tuned signature -- prefer qualified names;

tuned signature;

tuned message;

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;

prefer explicit Keyword.keywords;

eliminated pointless dynamic keywords (TTY legacy);

explicit type Keyword.keywords;
tuned signature;

recover via scanner;
tuned signature;

simplified -- scanning is never interactive;

added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};

tuned signature -- define some elementary operations earlier;

careful when calling 'Thm.proof_body_of' -- it can throw exceptions

peek instead of joining -- is perhaps less risky

generate backquotes without markup, since this confuses preplay; bump up spying version identifier;

optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)

more generous max number of suggestions, for more safety

reverted '|' features in MaSh -- these sounded like a good idea but never really worked

merged 'reconstructors' and 'proof methods'

generalized preplaying infrastructure to store various results for various methods

tuning

tuning

made timeouts in Sledgehammer not be 'option's -- simplified lots of code

generate problems with type classes

made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms

more Sledgehammer spying -- record fact indices

encode goal digest in spying log (to detect duplicates)

added "spy" option to Sledgehammer

removed |>! and #>!

added |>! and #>! for convenient printing of timing information

completely rewrote SH compress; added two parameters for experimentation/fine grained control

prefer explicitly qualified exceptions, which is particular important for robust handlers;

implement (more) accurate computation of parents

tuned data structure

thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices

refined class handling, to prevent cycles in fact graph

learn from low-level, inside-class facts

better weight functions for MePo/MaSh etc.

thread no timeout properly

merge aliased theorems in MaSh dependencies, modulo symmetry of equality

moved thms_of_name to Sledgehammer_Util and removed copies, updated references

avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit

centralized term printing code

cleaner temporary file cleanup for MaSh, based on tried-and-trusted code

added "learn_from_atp" command to MaSh, for patient users

learn command in MaSh

more consolidation of MaSh code

drastic overhaul of MaSh data structures + fixed a few performance issues

more code rationalization in relevance filter

moved most of MaSh exporter code to Sledgehammer

clarified Keyword.is_keyword: union of minor and major;
misc tuning and simplification;

first step in sharing more code between ATP and Metis translation

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML => src/HOL/Tools/ATP/atp_reconstruct.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML => src/HOL/Tools/ATP/atp_translate.ML

normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages

try both "metis" and (on failure) "metisFT" in replay

show time taken for reconstruction

use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)

merge timeout messages from several ATPs into one message to avoid clutter

fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context

eliminated more code duplication in Nitrox

improved Waldmeister support -- even run it by default on unit equational goals

improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything

reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts

improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types

query typedefs as well for monotonicity

exploit inferred monotonicity

discontinued special treatment of structure Lexicon;

no need to do a super-duper atomization if Metis fails afterwards anyway

instantiate induction rules automatically

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

standardize on seconds for Nitpick and Sledgehammer timeouts

finished renaming file and module

rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"

--HG--
rename : src/HOL/Tools/Sledgehammer/clausifier.ML => src/HOL/Tools/Sledgehammer/meson_clausifier.ML

added XML.content_of convenience -- cover XML.body, which is the general situation;

move functions around

avoid code duplication

speed up helper function

implemented Auto Sledgehammer

improve SPASS hack, when a clause comes from several facts

consider "locality" when assigning weights to facts

make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts

clean handling of whether a fact is chained or not;
more elegant and reliable than encoding it in the name

quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")

perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes

beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
another consequence of the transition to FOF

fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization

minor refactoring

complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"

generate full first-order formulas (FOF) in Sledgehammer

keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
this is rather involved because the Flotter FOF-to-CNF translator is normally implicit.
We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.

exploit "Name.desymbolize" to remove some dependencies

removed Sledgehammer's support for the DFG syntax;
this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.

expect SPASS 3.7, and give a friendly warning if an older version is used

honor "xsymbols"

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

expand combinators in Isar proofs constructed by Sledgehammer;
this requires shuffling around a couple of functions previously defined in Refute

parentheses around nested cases

unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)

support Vampire definitions of constants as "let" constructs in Isar proofs

fix types of "fix" variables to help proof reconstruction and aid readability

introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure

remove some bloat

Sledgehammer: the empty set of fact () should mean nothing, not unchanged

added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)

store nonmangled names along with mangled type names in Sledgehammer for debugging purposes

make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second

get rid of Polyhash, since it's no longer used

added options to Sledgehammer;
syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional