isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

use different name for debugging purposes
2010-08-23, by blanchet
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
2010-08-23, by blanchet
"no_atp" fact that leads to unsound Sledgehammer proofs
2010-08-23, by blanchet
"no_atp" fact that leads to unsound proofs in Sledgehammer
2010-08-23, by blanchet
"no_atp" fact that leads to unsound proofs
2010-08-23, by blanchet
"no_atp" a few facts that often lead to unsound proofs
2010-08-23, by blanchet
play with fudge factor + parse one more Vampire error
2010-08-23, by blanchet
fiddle a bit with the SPASS fudge number
2010-08-23, by blanchet
be more generous towards SPASS's -SOS mode
2010-08-22, by blanchet
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
2010-08-22, by blanchet
merged
2010-08-23, by haftmann
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-08-23, by haftmann
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
2010-08-23, by wenzelm
sporadic locking of jEdit buffer;
2010-08-23, by wenzelm
main session actor as independent thread, to avoid starvation via regular worker pool;
2010-08-23, by wenzelm
optional daemon flag;
2010-08-23, by wenzelm
tuned;
2010-08-23, by wenzelm
module for simplified thread operations (Scala version);
2010-08-23, by wenzelm
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
2010-08-23, by wenzelm
recognize more "smlnj" variants;
2010-08-23, by wenzelm
merged
2010-08-23, by wenzelm
treat "using X by metis" (more or less) the same as "by (metis X)"
2010-08-22, by blanchet
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
2010-08-22, by blanchet
merged
2010-08-22, by blanchet
more work on finite axiom detection
2010-08-22, by blanchet
revert junk submitted by mistake
2010-08-22, by blanchet
make sure minimizer facts go through "transform_elim_theorems"
2010-08-20, by blanchet
use a smaller simpset in order to not solve refl-instances
2010-08-22, by Christian Urban
allow for pre-simplification of lifted theorems
2010-08-22, by Christian Urban
changed to a more convenient argument order
2010-08-22, by Christian Urban
merged
2010-08-20, by haftmann
split and enriched theory SetsAndFunctions
2010-08-20, by haftmann
more concise characterization of of_nat operation and class semiring_char_0
2010-08-20, by haftmann
inj_comp and inj_fun
2010-08-20, by haftmann
tuned: less formal noise in Named_Target, more coherence in Class
2010-08-20, by haftmann
remove trivial facts
2010-08-20, by blanchet
unbreak "only" option of Sledgehammer
2010-08-20, by blanchet
merged
2010-08-20, by blanchet
improve "x = A | x = B | x = C"-style axiom detection
2010-08-20, by blanchet
temporarily disable "fequal" handling in Metis;
2010-08-20, by blanchet
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
2010-08-20, by blanchet
merged
2010-08-20, by blanchet
improve "x = A | x = B | x = C"-style fact discovery
2010-08-20, by blanchet
transform elim theorems before filtering "bool" and "prop" variables out;
2010-08-20, by blanchet
more fiddling with Sledgehammer's "add:" option
2010-08-20, by blanchet
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
2010-08-20, by blanchet
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
2010-08-19, by blanchet
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
2010-08-19, by blanchet
fix atomize
2010-08-19, by blanchet
improve atomization
2010-08-19, by blanchet
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
2010-08-19, by blanchet
added entries
2010-08-19, by blanchet
update docs
2010-08-19, by blanchet
tuning
2010-08-19, by blanchet
parse SNARK proofs
2010-08-19, by blanchet
added remote SInE and remote SNARK
2010-08-19, by blanchet
no spurious trailing "\n" at the end of Sledgehammer's output
2010-08-19, by blanchet
don't get confused by wrong slice
2010-08-18, by blanchet
make sure that "add:" doesn't influence the relevance filter too much
2010-08-18, by blanchet
tuning of relevance filter
2010-08-18, by blanchet

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle