| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "try" "try_methods"
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "metis_timeout" to "preplay_timeout" and continued implementation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor fixes to Sledgehammer docs
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
shorten minimizer command further, exploiting until-now-undocumented syntax
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor tweaks to the Nitpick documentation
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
added syntax for specifying Metis timeout (currently used only by SMT solvers)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
readded Waldmeister as default to the documentation and other minor changes
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
reintroduced Waldmeister but limit the number of remote threads created
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor doc adjustments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
make output more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
merge timeout messages from several ATPs into one message to avoid clutter
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
mention contributions from LCP and explain metis and metisFT encodings
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fixed trivial fact detection
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
cleaner handling of equality and proxies (esp. for THF)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
recognize more ATP failures
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fully support all type system encodings in typed formats (TFF, THF)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
take out Waldmeister from default for now -- success rate too low on Judgment Day
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
document relevance filter a bit more
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
|
changeset |
files
|
| Thu, 26 May 2011 23:21:00 +0200 |
noschinl |
instance inat for complete_lattice
|
changeset |
files
|
| Thu, 26 May 2011 22:02:40 +0200 |
boehmes |
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)
|
changeset |
files
|
| Thu, 26 May 2011 20:51:03 +0200 |
hoelzl |
integral strong monotone; finite subadditivity for measure
|
changeset |
files
|
| Thu, 26 May 2011 20:49:56 +0200 |
hoelzl |
composition of convex and measurable function is measurable
|
changeset |
files
|
| Thu, 26 May 2011 17:59:39 +0200 |
hoelzl |
introduce independence of two random variables
|
changeset |
files
|
| Thu, 26 May 2011 17:40:01 +0200 |
hoelzl |
add lemma indep_distribution_eq_measure
|
changeset |
files
|
| Thu, 26 May 2011 14:12:06 +0200 |
hoelzl |
add lemma indep_rv_finite
|
changeset |
files
|
| Thu, 26 May 2011 14:12:03 +0200 |
hoelzl |
generalize setsum_cases
|
changeset |
files
|
| Thu, 26 May 2011 14:12:02 +0200 |
hoelzl |
add lemma borel_0_1_law
|
changeset |
files
|