removed experimental encoding for Waldmeister

isabelle update -u control_cartouches;

add reconstruction by veriT in method smt

don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)

tuned signature: more operations;

killed final stops in Sledgehammer and friends

tuned signature;

prefer infix operations;

avoid error in Isar proof reconstruction if no ATP proof is available

removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs

SPASS-Pirate is now called Pirate

--HG--
rename : src/HOL/Tools/ATP/scripts/remote_spass_pirate => src/HOL/Tools/ATP/scripts/remote_pirate

discontinued obsolete Output.urgent_message;

improved handling of extensionality in Isar proofs generated from LEO-II and Satallax

more precise lemma insertion

insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem

eliminate duplicate hypotheses (which can arise due to (un)clausification)

'moura' method is also useful for reconstructing skolemization of lambda-lifting of formulas for other provers than Z3

tuning

removed accidental '@{print}'

Some work on the new waldmeister integration

renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods

removed show stuttering

try 'skolem' method first for Z3

added 'skolem' method, esp. for 'obtain's generated from Z3 proofs

renamed new SMT module from 'SMT2' to 'SMT'

--HG--
rename : src/HOL/SMT2.thy => src/HOL/SMT.thy
rename : src/HOL/Tools/SMT2/smt2_builtin.ML => src/HOL/Tools/SMT/smt_builtin.ML
rename : src/HOL/Tools/SMT2/smt2_config.ML => src/HOL/Tools/SMT/smt_config.ML
rename : src/HOL/Tools/SMT2/smt2_datatypes.ML => src/HOL/Tools/SMT/smt_datatypes.ML
rename : src/HOL/Tools/SMT2/smt2_failure.ML => src/HOL/Tools/SMT/smt_failure.ML
rename : src/HOL/Tools/SMT2/smt2_normalize.ML => src/HOL/Tools/SMT/smt_normalize.ML
rename : src/HOL/Tools/SMT2/smt2_real.ML => src/HOL/Tools/SMT/smt_real.ML
rename : src/HOL/Tools/SMT2/smt2_solver.ML => src/HOL/Tools/SMT/smt_solver.ML
rename : src/HOL/Tools/SMT2/smt2_systems.ML => src/HOL/Tools/SMT/smt_systems.ML
rename : src/HOL/Tools/SMT2/smt2_translate.ML => src/HOL/Tools/SMT/smt_translate.ML
rename : src/HOL/Tools/SMT2/smt2_util.ML => src/HOL/Tools/SMT/smt_util.ML
rename : src/HOL/Tools/SMT2/smtlib2.ML => src/HOL/Tools/SMT/smtlib.ML
rename : src/HOL/Tools/SMT2/smtlib2_interface.ML => src/HOL/Tools/SMT/smtlib_interface.ML
rename : src/HOL/Tools/SMT2/smtlib2_isar.ML => src/HOL/Tools/SMT/smtlib_isar.ML
rename : src/HOL/Tools/SMT2/smtlib2_proof.ML => src/HOL/Tools/SMT/smtlib_proof.ML
rename : src/HOL/Tools/SMT2/verit_isar.ML => src/HOL/Tools/SMT/verit_isar.ML
rename : src/HOL/Tools/SMT2/verit_proof.ML => src/HOL/Tools/SMT/verit_proof.ML
rename : src/HOL/Tools/SMT2/verit_proof_parse.ML => src/HOL/Tools/SMT/verit_proof_parse.ML
rename : src/HOL/Tools/SMT2/z3_new_interface.ML => src/HOL/Tools/SMT/z3_interface.ML
rename : src/HOL/Tools/SMT2/z3_new_isar.ML => src/HOL/Tools/SMT/z3_isar.ML
rename : src/HOL/Tools/SMT2/z3_new_proof.ML => src/HOL/Tools/SMT/z3_proof.ML
rename : src/HOL/Tools/SMT2/z3_new_real.ML => src/HOL/Tools/SMT/z3_real.ML
rename : src/HOL/Tools/SMT2/z3_new_replay.ML => src/HOL/Tools/SMT/z3_replay.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_literals.ML => src/HOL/Tools/SMT/z3_replay_literals.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_methods.ML => src/HOL/Tools/SMT/z3_replay_methods.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_rules.ML => src/HOL/Tools/SMT/z3_replay_rules.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_util.ML => src/HOL/Tools/SMT/z3_replay_util.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
rename : src/HOL/Word/Tools/smt2_word.ML => src/HOL/Word/Tools/smt_word.ML

rationalize Skolem names

tuning

tuning

deal with E definitions

cleaner 'compress' option

tuned terminology (cf. 'isar_proofs' option)

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

refined filter for ATP steps to avoid 'have True' steps in E proofs

'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)

better duplicate detection

normalize conjectures vs. negated conjectures when comparing terms

tweaked 'clone' formula detection

fine-tuned Isar reconstruction, esp. boolean simplifications

centralized boolean simplification so that e.g. LEO-II benefits from it

better handling of variable names

nicer generated variable names

tuning

tuning

more precise handling of LEO-II skolemization

beware of 'skolem' rules that do not skolemize (e.g. LEO-II)

added appropriate method for skolemization of Z3 steps to the mix

tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence

tuning

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

Skolemization for tmp_ite_elim rule in the SMT solver veriT.

Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.

Whitespace and indentation correction.

imported patch hilbert_choice_support

veriT changes for lifted terms, and ite_elim rules.

Subproofs for the SMT solver veriT.

Basic support for the SMT prover veriT.

Skolemization support for leo-II and Zipperposition.

also try 'metis' with 'full_types'

supports gradual skolemization (cf. Z3) by threading context through correctly

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

renamed Sledgehammer options

basic setup for zipperposition prover

properly reconstruct helpers in Z3 proofs

tuning

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

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

added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')

consolidate consecutive steps that prove the same formula

undo rewrite rules (e.g. for 'fun_app') in Isar

debugging stuff

more simplification of trivial steps

tuning

tuning

simplified preplaying information

integrate SMT2 with Sledgehammer

tuned signature;

avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures

more generous Isar proof compression -- try to remove failing steps

do a second phase of proof compression after minimization

tuned code

split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)

rationalized lists of methods

extended method list

generate comments in Isar proofs

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

tuned behavior of 'smt' option

proper fresh name generation

tuned data structure

tuned data structure

less aggressive evaluation

added a new version of 'metis' to the mix

implemented new 'try0_isar' semantics

got rid of 'try0' step that is now redundant

centralize more preplaying

centralize preplaying

tuned

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

renamed ML file

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

tuning

merged 'reconstructors' and 'proof methods'

tuning

more data structure rationalization

more data structure rationalization

rationalized threading of 'metis' arguments

refactored data structure (step 3)

unform treatment of preplay_timeout = 0 and > 0

use Skolem proof methods appropriately

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

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

renamed Sledgehammer options for symmetry between positive and negative versions

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

fixed spying so that the envirnoment variables are queried at run-time not at build-time

tuning

added comment

use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available

run fewer provers in "try" mode

count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)

count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)

added "spy" option to Sledgehammer

merged "isar_try0" and "isar_minimize" options

hardcoded obscure option

hard-coded an obscure option

use configuration mechanism for low-level tracing

took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired

tuning (use a blacklist instead of a whitelist)

fixed subtle bug with "take" + thread overlord through

have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation

prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;

some protocol to determine provers according to ML;

always enable "minimize" to simplify interaction model;
override params more directly -- they are no longer echoed in minimize command;

sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
back to Normal mode: with output_result it is sufficient to determine TTY vs. PIDE operation;

eliminated pointless subgoal argument;

more direct sledgehammer configuration via mode = Normal_Result and output_result;
retain standard sledgehammer parallelization policies;

clarified Query_Operation.register: avoid hard-wired parallel policy;
sledgehammer: more conventional parallel exception handling -- print just one interrupt;

dockable window for Sledgehammer, based on asynchronous/parallel query operation;

hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);

system options for Isabelle/HOL proof tools;

added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases

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

make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation

added compatibility alias

tuning -- renamed '_from_' to '_of_' in Sledgehammer

clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;

maintain ProofGeneral preferences within ProofGeneral module;
initialize Isabelle/Pure preferences within normal user space (with antiquotations);
tuned;

renamed Sledgehammer functions with 'for' in their names to 'of'

just one ProofGeneral module;

--HG--
rename : src/Pure/ProofGeneral/proof_general_emacs.ML => src/Pure/ProofGeneral/proof_general.ML

added preplay tracing

more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);

minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay

fixed typo in option name

made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired

alias for people like me

killed legacy alias

renamed sledgehammer_shrink to sledgehammer_compress

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML => src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML

tuned

set show_markup to false in order to avoid problems in jedit

nicer output

pass option to minimize

renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)

crank up default timeout for MaSh ATP learning

thread no timeout properly

adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)

create temp directory if not already created

renamed Sledgehammer option

renamed Isar-proof related options + changed semantics of Isar shrinking

tuned message

merged two commands

detect unknown options again

don't relearn old facts in Isar mode

took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks

honor suggested MaSh weights

use CVC3 and Yices by default if they are available and there are enough cores

minimal maxes + tuning

learn from SMT proofs when they can be minimized by Metis

convenience

learning should honor the fact override and the chained facts

added "learn_from_atp" command to MaSh, for patient users

more MaSh docs

learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds

learn command in MaSh

renamed ML structures

optimize parent computation in MaSh + remove temporary files

learn from minimized ATP proofs

use async manager to manage MaSh learners to make sure they get killed cleanly

added option to control which fact filter is used

make tracing an option

more implementation work on MaSh

started implementing MaSh client-side I/O

renamed Sledgehammer options

more code rationalization in relevance filter

further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)

lower the monomorphization thresholds for less scalable provers

swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations

improve "remote_satallax" by exploiting unsat core

made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release

added "dont_preplay" alias

outer syntax command definitions based on formal command_spec derived from theory header declarations;

prefer formally checked @{keyword} parser;

renamed type encoding

made option available to users (mostly for experiments)

include new SPASS by default if available

renamed two files to make room for a new file

--HG--
rename : src/HOL/Tools/ATP/atp_translate.ML => src/HOL/Tools/ATP/atp_problem_generate.ML
rename : src/HOL/Tools/ATP/atp_reconstruct.ML => src/HOL/Tools/ATP/atp_proof_reconstruct.ML
rename : src/HOL/Tools/ATP/atp_redirect.ML => src/HOL/Tools/ATP/atp_proof_redirect.ML
rename : src/HOL/Tools/Metis/metis_translate.ML => src/HOL/Tools/Metis/metis_generate.ML

renamed "sound" option to "strict"

lower timeout for preplay, now that we have more preplay methods

added "minimize" option for more control over automatic minimization

renamed "slicing" to "slice"

thread in additional options to minimizer

make metis reconstruction handling more flexible

parse lambda translation option in Metis

reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)

take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime

parse new experimental '@' encodings

tuning

rationalize uniform encodings

fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"

renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)

--HG--
rename : src/HOL/Tools/Metis/metis_tactics.ML => src/HOL/Tools/Metis/metis_tactic.ML

extended simple types with polymorphism -- the implementation still needs some work though

rationalized option names -- mono becomes raw_mono and mangled becomes mono

more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"

cleaner handling of polymorphic monotonicity inference

renamed E wrappers for consistency with CASC conventions

renamed "preds" encodings to "guards"

renamed "type_sys" to "type_enc", which is more accurate

added "sound" option to force Sledgehammer to be pedantically sound

removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway

removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them

fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day

killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"

parse optional type system specification

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

made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly

fixed syntax of min options

minimize with Metis if possible

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

prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators

handle non-auto try case of Sledgehammer better

added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods

renamed "Auto_Tools" "Try"

--HG--
rename : src/Tools/auto_tools.ML => src/Tools/try.ML

renamed "metis_timeout" to "preplay_timeout" and continued implementation

shorten minimizer command further, exploiting until-now-undocumented syntax

added syntax for specifying Metis timeout (currently used only by SMT solvers)

reintroduced Waldmeister but limit the number of remote threads created

renamed "minimize" to "min" to make Sledgehammer output a little bit more concise

take out Waldmeister from default for now -- success rate too low on Judgment Day

always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)

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

reduce the number of mono iterations to prevent the mono code from going berserk

added convenience syntax

renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly

ensure that Auto Sledgehammer is run with full type information

added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option

smoother handling of ! and ? in type system names

use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used

restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"

use ! for mildly unsound and !! for very unsound encodings

implement the new ATP type system in Sledgehammer

make sure the minimizer monomorphizes when it should

added (without implementation yet) new type encodings for Sledgehammer/ATP

tuning

cleanup: get rid of "may_slice" arguments without changing semantics

implemented general slicing for ATPs, especially E 1.2w and above

modernized structure Proof_Context;

renamed "const_args" option value to "args"

killed unimplemented type encoding "preds"

if "monomorphize" is enabled, mangle the type information in the names by default

added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default

available_provers ~> supported_provers (for clarity)

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented

make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive

make "full_types" take precedence over "type_sys"

implemented partially-typed "tags" type encoding

implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound

added "type_sys" option to Sledgehammer

split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems

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

replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us

run synchronous Auto Tools in parallel

enabled SMT solver in Sledgehammer by default

use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);

use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
updated docs

standardize on seconds for Nitpick and Sledgehammer timeouts

integrated "smt" proof method with Sledgehammer

tuning

make SML/NJ happy

make "sledgehammer_params" work on single-threaded platforms

more robust handling of "remote_" vs. non-"remote_" provers

fixed signature of "is_smt_solver_installed";
renaming

took out "smt"/"remote_smt" from default ATPs until they are properly implemented

make Sledgehammer minimizer fully work with SMT

first step in adding support for an SMT backend to Sledgehammer

use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."

use 30 s instead of 60 s as the default Sledgehammer timeout;
very few proofs are lost this way (esp. thanks to the parallel use of provers, cf. Boehme & Nipkow 2010), and this is much more tolerable for users

tuning

finished renaming "Auto_Counterexample" to "Auto_Tools"

implemented Auto Sledgehammer

got rid of the "theory_relevant" option;
instead, have fudge factors that behave more smoothly for all provers

generalize theorem argument parsing syntax

finished renaming

added "expect" feature of Nitpick to Sledgehammer, for regression testing

added "blocking" option to Sledgehammer to run in synchronous mode;
sometimes useful, e.g. for testing

add a penalty for being higher-order

make Sledgehammer's relevance filter somewhat slacker

reorganize options regarding to the relevance threshold and decay

make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
"max_relevant" is more reliable than "max_relevant_per_iter";
also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before;
SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)

get rid of "defs_relevant" feature;
nobody uses it and it works poorly

renamed "relevance_convergence" to "relevance_decay"

invert semantics of "relevance_convergence", to make it more intuitive

if no facts were selected on first iteration, try again with a lower threshold

get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"

added "max_relevant_per_iter" option to Sledgehammer

move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML => src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML

use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
this replaces the previous, somewhat messy solution of adding "extra" clauses

minor refactoring

minor refactoring

minor refactoring

rename "ATP_Manager" ML module to "Sledgehammer";
more refactoring to come

renamings + only need second component of name pool to reconstruct proofs

always perform "inline" skolemization, polymorphism or not, Skolem cache or not

always perform relevance filtering on original formulas

factor out thread creation

got rid of "respect_no_atp" option, which even I don't use

renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)

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

further reduce dependencies on "sledgehammer_fact_filter.ML"

killed legacy "neg_clausify" and "clausify"

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

proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter

totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
faster and more reliable

made "clausify" attribute a legacy feature;
seems to have ever only been a debugging feature

made "neg_clausify" a legacy feature

kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output

make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work

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

renamed options

renamed two Sledgehammer options

delect installed ATPs dynamically, _not_ at image built time

made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)

remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
what we need is smarter type annotations for variables _and_ constants

make Sledgehammer more friendly if no subgoal is left

remove "higher_order" option from Sledgehammer -- the "smart" default is good enough

rename options

cosmetics

move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"

remove some bloat

renamed module "ATP_Wrapper" to "ATP_Systems"

move the minimizer to the Sledgehammer directory

--HG--
rename : src/HOL/Tools/ATP_Manager/atp_minimal.ML => src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML

move some sledgehammer stuff out of "atp_manager.ML"

move the Sledgehammer menu options to "sledgehammer_isar.ML"

remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed

pass relevant options from "sledgehammer" to "sledgehammer minimize";
one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files

added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)

make Sledgehammer's minimizer also minimize Isar proofs

rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does

by default, don't try to start ATPs that aren't installed

fiddle with Sledgehammer option syntax

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

added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture

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

make Sledgehammer's "timeout" option work for "minimize"

fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
and added "atp" as alias for "atps"

added "modulus" and "sorts" options to control Sledgehammer's Isar proof output

make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"

made "theory_const" a Sledgehammer option;
by default, it's true for SPASS and false for the others. This eliminates the need for the "spass_no_tc" ATP, which can be obtained by passing "no_theory_const" instead.

added "respect_no_atp" and "convergence" options to Sledgehammer;
these were previously hard-coded in "sledgehammer_fact_filter.ML"

make SML/NJ happy

make Mirabelle happy again

revert debugging output that shouldn't have been submitted in the first place

honor the newly introduced Sledgehammer parameters and fixed the parsing;
e.g. the prover "e_isar" (formely "e_full") is gone, instead do sledgehammer [atps = e, isar_proof] to get the same effect

added a syntax for specifying facts to Sledgehammer;
e.g., sledgehammer (add: foo del: bar)
which tells the relevance filter to include "foo" but omit "bar".

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

make "sledgehammer" and "atp_minimize" improper commands

move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later