misc tuning;

formal check of jEdit actions;

more on "Completion";

more on "Completion";

tuned;

clarified role of old user interfaces as misc tools;

added Index;

more on "Completion";

more on "Completion";

tuned;

more on "Completion";

more on "Completion";

more on "Auxiliary files";

more on "Document model";

suppress index;

more on command-line invocation -- moved material from system manual;

clarified section structure;

clarified section structure;

clarified section structure;

more on dockable windows;

clarified section structure;

tuned;

more on Query panel;

updated screenshots;

more on Query panel -- updated Find Theorems;

misc tuning and updates;

merged

add lemma

tuning

optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)

minor table access optimization

document property 'rel_coinduct'

tune the implementation of 'rel_coinduct'

generate 'rel_coinduct' theorem for codatatypes

generate 'rel_coinduct0' theorem for codatatypes

added parentheses around type arguments in THF

optimize log

enable TF-IDF

added another experimental engine

tweaked experimental setup

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