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"

encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed

fix atomize

improve atomization

fix SInE's error handling + run "vampire" locally if either SPASS or E is missing

added entries

update docs

tuning

parse SNARK proofs

added remote SInE and remote SNARK

no spurious trailing "\n" at the end of Sledgehammer's output

don't get confused by wrong slice

make sure that "add:" doesn't influence the relevance filter too much

tuning of relevance filter

minor cleanup

bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")

update docs

get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"

added "max_relevant_per_iter" option to Sledgehammer

thank Andrei instead of Tanya

fix the relevance filter so that it ignores If, Ex1, Ball, Bex

tuning

reactivated -segprot options, just to make double-sure;

tuned Markup_Tree.+ : slightly more expensive version to rebuild rest avoids crash of RedBlack.scala:120 (version Scala 2.8.0), e.g. on the following input: ML {* fun f x = (x + 1, "aaa") *}

tuned;

tuned signature;

simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);

proper range for hyperlinks and tooltips, using original markup information;

tuned signature;

misc tuning and simplification;

renamed Markup_Tree.Node to Text.Info; Markup_Tree.select: body may depend on full Text.Info, including range; tuned;

removed obsolete Markup_Tree.flatten/filter;

Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;

Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;

tuned signatures;

Command.State: accumulate markup reports uniformly; Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo; tuned;

Markup_Tree.select: misc simplification, proper restriction of parent in subtree;

added Text.Range.- convenience;

tuned signatures;

alternative constructor for Range singularities;

concentrate protocol message formats in Isar_Document;

Branches.overlapping: proper treatment of stop_range that overlaps with end; Markup_Tree.select: allow singularity in parent range specification;

further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;

parameterized type Markup_Tree.Node; Markup_Tree.select: allow arbitrary interpretations, not just filtering; renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps;

added toString methods;

misc tuning and simplification;

updated some isatest settings;

added generated file;

merged

tuned quotes

more antiquotations

deglobalized named HOL constants

deglobalized named HOL constants

corrected some long-overseen misperceptions in recdef

use HOLogic.boolT and @{typ bool} more pervasively

tuned

some more antiquotations

tuned

use antiquotations for remaining unqualified constants in HOL

tuned

tuned declaration order

merged

NEWS

re-added instantiation of type class random for records

tuned signature and code

adjusted to restored naming convention of logical record types

robustified proof

adjusted to changed naming convention of logical record types

removed separate quickcheck_record module

liberal instantiation of class eq; tuned naming scheme

more helpful NEWS entry

dropped SML typedef_codegen: does not fit to code equations for record operations any longer

preemptive NEWS