merged

introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets

added support for xsymbol syntax for mode annotations in code_pred command

tuned raw Sidekick output;

Text.Range.is_singleton;

Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;

tuned;

Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree; tuned;

tuned root markup;

misc tuning of important special cases;

Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.

merged

merged

use different name for debugging purposes

perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes

"no_atp" fact that leads to unsound Sledgehammer proofs

"no_atp" fact that leads to unsound proofs in Sledgehammer

"no_atp" fact that leads to unsound proofs

"no_atp" a few facts that often lead to unsound proofs

play with fudge factor + parse one more Vampire error

fiddle a bit with the SPASS fudge number

be more generous towards SPASS's -SOS mode

don't penalize abstractions in relevance filter + support nameless `foo`-style facts

merged

dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates

Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);

sporadic locking of jEdit buffer;

main session actor as independent thread, to avoid starvation via regular worker pool; tuned;

optional daemon flag;

tuned;

module for simplified thread operations (Scala version);

added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);

recognize more "smlnj" variants;

merged

treat "using X by metis" (more or less) the same as "by (metis X)"

prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible; the disjunctive view of "conjecture" is nonstandard but taken by E, SPASS, Vampire, etc.

merged

more work on finite axiom detection

revert junk submitted by mistake

make sure minimizer facts go through "transform_elim_theorems"

use a smaller simpset in order to not solve refl-instances

allow for pre-simplification of lifted theorems

changed to a more convenient argument order

merged

split and enriched theory SetsAndFunctions

more concise characterization of of_nat operation and class semiring_char_0

inj_comp and inj_fun

tuned: less formal noise in Named_Target, more coherence in Class

remove trivial facts

unbreak "only" option of Sledgehammer

merged

improve "x = A | x = B | x = C"-style axiom detection

temporarily disable "fequal" handling in Metis; one proof fails in "HOL-Auth" because of the new rules

use "hypothesis" rather than "conjecture" for hypotheses in TPTP format; avoids relying on inconsistently implemented feature of TPTP format

merged

improve "x = A | x = B | x = C"-style fact discovery

transform elim theorems before filtering "bool" and "prop" variables out; another consequence of the transition to FOF

more fiddling with Sledgehammer's "add:" option

beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly); another consequence of the transition to FOF

generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"