changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)

use strings to communicate with external process, to ease debugging

added 'dummy_thf_ml' prover for experiments with HOLyHammer

phantoms may also occur in THF1

added experimental MaSh engine

move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects

help reconstruction of Z3 skolemization by weakening formulas a bit

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

don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)

r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs

added [simp]

Two basic lemmas on bij_betw.

changed default MaSh parameters based on (in vitro) evaluation

made 'tptp_graph' more liberal (why reject TFF?)

made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'

more MaSh engine variations, for evaluations

split parameter into two

filters are easier to define with INF on filters.

moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin

more generous formula -- there are lots of duplicates out there

automatically learn MaSh facts also in 'blocking' mode

enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable

Lemmas contributed by Joachim Breitner.

reintroduce atomize in Waldmeister code

changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas

compile

integrated new Waldmeister code with 'sledgehammer' command

fixed parsing of one-argument 'file()' in TSTP files

use right delimiters for Waldmeister proofs

added 'waldmeister_new' as ATP

simplified code

moved code around

give Z3 TPTP proofs a chance

fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)

add more derivative and continuity rules for complex-values functions

Moving the remote prefix deleting on Sledgehammer's side

Correcting the type parser

imported patch leo2_skolem_simplication

add support for Isar reconstruction for thf1 ATP provers like Leo-II.

lemmas about the moments of the normal distribution

NEWS

properties of normal distributed random variables (by Sudeep Kanav)

announce Tree

new theory of binary trees

formal variable name: IVar NONE is strictly spoken not supported on lhs of function definitions, e.g. in Scala

merged

added [simp]

tuning

renamed Sledgehammer options

removed dead code

reintroduced vital 'Thm.transfer'

tuned dependencies

updated docs

added support for CVC4 in SMT2

don't ask proof-disabled solvers to do proofs

tuning

took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale

made CVC3 work with SMT2 stack

properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)

clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin

uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor

adapted examples to changes in SMT triggers

reduces Sledgehammer dependencies

eliminate dependency of SMT2 module on 'list'

tuning

removed subsumed record-related code, now that records are registered as 'ctr_sugar'

made lookup more robust in the face of missing (dummy) case constant

use 'ctr_sugar' abstraction in SMT(2)

register record extensions as freely generated types

mixin definitions are within scope of "for"s of import expression

proper proof context transfer wrt. background theory avoids ad-hoc restore operation

refactoring

moved generic code further up

tuned code

factor out SMT-LIB 2 type/term parsing from Z3-specific code

simplify slightly ATP proof generated for Z3

tuned whitespaces

updated contributors to include students

moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle

adapted SMT examples to new, corrected handling of 'typedef'

fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective

updated NEWS slightly

updated docs w.r.t. Z3

rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions

removed '_new' sufffix in SMT2 solver names (in some cases)

removed old SMT module from Sledgehammer

got rid of 'listF' example, which is now subsumed by the real 'list' type

changed syntax of map: and rel: arguments to BNF-based datatypes

tuning

updated Z3 certificates

generate ':named' attributes in SMT-LIB 2 problems, to facilitate reconstruction

tuning

add type class instances for unit

use 'where' clause for selector default value syntax