added argo

avoid legacy binding errors in Sledgehammer Isar proofs

parse applie lambdas correctly plus deal gracefully with lambda-lifting in…

allow (~) syntax in TPTP proofs for unapplied negation

reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs

use same associativity as Isabelle when parsing HOL proofs

improved Sledgehammer's HOL proof parser w.r.t. negation

tuned Sledgehammer messages

respect timeout better

avoid using FOOL syntax with older Vampire versions because of soundness bug…

avoid using FOOL syntax with older Vampire versions because of soundness bug…

disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't…

made 'primcorec' more robust

small simplifications

shortened some parts of Huffman proof using Sledgehammer

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…