removed accidental junk

use simplifier to classify the missing assumptions in Sledgehammer's abduction…

don't try to falisfy goals with schematics

require the presence of free variables to do abduction in Sledgehammer

detect duplicates in Sledgehammer output -- suggested by Larry Paulson

got rid of 'important message' mechanism in SystemOnTPTP (which is less used…

tweaked Sledgehammer interaction

there won't be an E version 2.7

compile

adopt terminology suggested by Larry Paulson

reverted 0506c3273814 -- the message is still useful

more robust E proof parsing

tweaked abduction in Sledgehammer

avoid double 'Warning:' in Sledgehammer messages

slightly more documentation

renamed new Sledgehammer option

updated documentation

improve ad hoc abduction in Sledgehammer

tuning

implemented ad hoc abduction in Sledgehammer with E

don't apply abduction and consistency checking to goals of the form 'False'

tuned metis call to avoid obscure feature

removed rarely used error in Sledgehammer

added refute mode to Sledgehammer to find 'counterexamples'

updated NEWS

careful eta-contraction in Metis to keep argument to All and Ex expanded

added lifting_forget as suggested by Peter Lammich

merge

adapted to Isabelle/c48fe2be847f

compile

correctly show '(> 2 s, timed out)' or similar in Sledgehammer's output

use timeout with MiniSat

generate some metainformation not only for SPASS but also for Zipperposition…

added a bound in SMT on the number of schematic constants considered -- the…

replaced slow smt call by blast

tuning

reintroduced SPASS to the mix

tweaked generation of Isar proofs

tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and…

revived 'try0' and 'smart' Isar proofs in Sledgehammer

added support for cvc5 (whose interface is almost identical to CVC4)

more accurate name

more politically correct

added two lemmas to relational chains

merge

changed the order of Zipperposition slices in Sledgehammer

changed confusing assumption name

removed a spurious locale parameter -- the same issue probably arises in the…

removed needless assumption

added lemma about lazy list chains

typo

prefer non-JNI SAT solvers by default in Nitpick

milder Sledgehammer messages

pass new option only to new version of E

enable an E option suggested by Petar Vukmirovic

merge

tuned slices to get the fifth Zipperposition slice in a typical run

further tweaked E's setup

tweaked E setup

nicer TPTP output

compile TPTP module

compile mirabelle

further modernized E setup

cleaned up obsolete E setup and a bit of SPASS

second and last step in making time slicing more flexible in Sledgehammer: try…

first step in making time slicing more flexible in Sledgehammer: label slices…

added parentheses in TPTP output -- seem necessary for some provers

have Sledgehammer honor 'smt_nat_as_int' option

handle Zipperposition definitions in Isar proof construction

more handling of Zipperposition definitions in Isar proof construction

parse Zipperposition definitions

print outcome of Sledgehammer search in panel

print Sledgehammer error message

more liberal parsing of Sledgehammer options to allow empty lists (as suggested…

more robust TSTP proof parsing

added possibility of extra options to SMT slices

more precise slicing computation and output when not enough lemmas are…

enable induction in one of Zipperposition's slices

made sorting of Vampire facts more robust in the face of names that deviate…

robustly handle empty proof blocks in Isar proof output

propagate right result when enough proofs have been found

don't lose error messages

correctly parse E proofs that assume '=' and '!=' bind more tightly than…

don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in…

don't perform preplaying steps if preplaying is disabled

careful with partial applications

tuned punctuation

adjust TPTP THF parser to give priority to @ over other operators, to parse…

handle TPTP '!=' more gracefully in Isar proof reconstruction

guard against duplicate lines in Zipperposition proofs

compile HOL-TPTP

tuning

tuned NEWS

compile Metis_Examples

more NEWS

updated NEWS

compile mirabelle

tweaked Auto Sledgehammer's behavior and output

removed experimental prover z3_tptp