set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed

minor code cleanup

if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing

"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing

Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes; this solves the unification exception that consistently was thrown for Cezary's "FSet3" theory

postprocess ATP output in "overlord" mode to make it more readable

failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is

generate command-line in addition to timestamp in ATP output file, for debugging purposes

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

Finite set theory

merged

Tidied up using s/l

split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;

fun_rel introduction and list_rel elimination for quotient package

lemmas concerning remdups

lemma dlist_ext

merged

optionally ignore errors during translation of equations; tuned representation of abstraction points

optionally ignore errors during translation of equations

tolerate eta-variants in f_graph.cases (from inductive package); added test case;

simplified example

use only one thread in "Manual_Nits"; the second thread isn't helping much, and might very well be the cause of the Cygwin Isatest failure

merged

clarify error message

distinguish between the different ATP errors in the user interface; in particular, tell users to upgrade their SPASS if they try to run "spass_tptp" with an old SPASS version with no TPTP support

added "spass_tptp" prover, which requires SPASS x.y > 3.0; once users have upgraded their SPASS and we have determined that "spass_tptp" works well, we can make "spass_tptp" the one and only "spass"

use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"

merged

make profiling depend on reference Quickcheck.timing

added examples for detecting switches

adopting documentation of the predicate compiler

removing dead code; clarifying function names; removing clone

adopting examples to changes in the predicate compiler

adopting quickcheck

tuning mutabelle; adding output of mutant theoryfile for interactive evaluation

added switch detection to the predicate compiler

added further inlining of boolean constants to the predicate compiler

adding more profiling to the predicate compiler

only add relevant predicates to the list of extra modes

switched off no_topmost_reordering

replaced call to inductive package by axiomatization in the function flattening of the predicate compiler

added option for specialisation to the predicate compiler

prefer functional modes of functions in the mode analysis

added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations

merged

Only use provided SMT-certificates in HOL-Multivariate_Analysis.

Translated remaining theorems about integration from HOL light.

marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);

replace many uses of Drule.export_without_context with Drule.zero_var_indexes

Remove garbage.

Remove garbage.

recovered isabelle java, which was broken in ebfa4bb0d50f;

fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared; this bug occurs when the explicit "hAPP" or "hBOOL" functions are introduced and full types is activated

merged

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)

merge

cosmetics

don't redo an axiom selection in the first round of Sledgehammer "minimize"!; this is needlessly slow and messes up the declared functions/predicates in SPASS DFG files

get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts

added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent