take out Waldmeister from default for now -- success rate too low on Judgment Day

document relevance filter a bit more

always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)

towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)

instance inat for complete_lattice

iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)

integral strong monotone; finite subadditivity for measure

composition of convex and measurable function is measurable

introduce independence of two random variables

add lemma indep_distribution_eq_measure

add lemma indep_rv_finite

generalize setsum_cases

add lemma borel_0_1_law

add lemma sigma_sets_singleton

use abbrevitation events == sets M

add lemma kolmogorov_0_1_law

add lemma indep_sets_collect_sigma

improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing

extending terms of Code_Evaluation by Free to allow partial terms

adhoc event handler to insert 'sendback' text into the buffer, replacing the original command

css rules for highlighting sendback text

invert event propagation flag -- in lobobrowser api, true means re-propagate

eta-expand to make SML/NJ happy

ensure that the argument of logical negation is enclosed in parentheses in THF mode

hack to obtain potable step names from Waldmeister

respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")

further reduce the number of facts passed to less used remote ATPs

added quietness flag

pass fewer relevant facts to less used remote systems

more work on parsing LEO-II proofs and extracting uses of extensionality

tuning

more work on parsing LEO-II proofs without lambdas

slightly gracefuller handling of LEO-II and Satallax output

document primitive support for LEO-II and Satallax

identify HOL functions with THF functions

started adding support for THF output (but no lambdas)

eliminated more code duplication in Nitrox

reduce code duplication in Nitrox

use \<emdash> rather than \<midarrow>

fixed de Bruijn index bug

use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things

filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations

clearer SystemOnTPTP errors

give fewer equations to Waldmeister

detect inappropriate problems and crashes better in Waldmeister

tuning -- the "appropriate" terminology is inspired from TPTP

pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding

move lemmas to Extended_Reals and Extended_Real_Limits

separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform

reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive

fun command produces warning when patterns are incomplete (somewhat analogous to primrec)

added message when Waldmeister isn't run

slightly improved documentation

improved Waldmeister support -- even run it by default on unit equational goals

fish out axioms in Waldmeister output

removed SNARK hack now that SNARK is fixed