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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
2011-05-29, by blanchet
function tutorial: do not omit termination proof, even when discussing other things
2011-05-27, by krauss
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
2011-05-27, by boehmes
document new "try"
2011-05-27, by blanchet
tuned comments
2011-05-27, by blanchet
new timeout section (cf. Nitpick manual)
2011-05-27, by blanchet
cleanup proof text generation code
2011-05-27, by blanchet
more Sledgehammer documentation updates
2011-05-27, by blanchet
minor update
2011-05-27, by blanchet
try both "metis" and (on failure) "metisFT" in replay
2011-05-27, by blanchet
show time taken for reconstruction
2011-05-27, by blanchet
unbreak "max_potential" logic
2011-05-27, by blanchet
more concise output
2011-05-27, by blanchet
compile
2011-05-27, by blanchet
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
2011-05-27, by blanchet
repaired theory merging and defined/used helpers
2011-05-27, by blanchet
make Sledgehammer a little bit less verbose in "try"
2011-05-27, by blanchet
handle non-auto try cases gracefully in Try Methods
2011-05-27, by blanchet
handle non-auto try case gracefully in Solve Direct
2011-05-27, by blanchet
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
2011-05-27, by blanchet
update SML section of documentation
2011-05-27, by blanchet
handle non-auto try case gracefully in Nitpick
2011-05-27, by blanchet
handle non-auto try case of Sledgehammer better
2011-05-27, by blanchet
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-27, by blanchet
removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
2011-05-27, by blanchet
renamed "Auto_Tools" "Try"
2011-05-27, by blanchet
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
2011-05-27, by blanchet
renamed "try" "try_methods"
2011-05-27, by blanchet
renamed "metis_timeout" to "preplay_timeout" and continued implementation
2011-05-27, by blanchet
minor fixes to Sledgehammer docs
2011-05-27, by blanchet
shorten minimizer command further, exploiting until-now-undocumented syntax
2011-05-27, by blanchet
minor tweaks to the Nitpick documentation
2011-05-27, by blanchet
added syntax for specifying Metis timeout (currently used only by SMT solvers)
2011-05-27, by blanchet
readded Waldmeister as default to the documentation and other minor changes
2011-05-27, by blanchet
reintroduced Waldmeister but limit the number of remote threads created
2011-05-27, by blanchet
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
2011-05-27, by blanchet
minor doc adjustments
2011-05-27, by blanchet
make output more concise
2011-05-27, by blanchet
merge timeout messages from several ATPs into one message to avoid clutter
2011-05-27, by blanchet
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
2011-05-27, by blanchet
tuning
2011-05-27, by blanchet
mention contributions from LCP and explain metis and metisFT encodings
2011-05-27, by blanchet
fixed trivial fact detection
2011-05-27, by blanchet
cleaner handling of equality and proxies (esp. for THF)
2011-05-27, by blanchet
recognize more ATP failures
2011-05-27, by blanchet
fully support all type system encodings in typed formats (TFF, THF)
2011-05-27, by blanchet
take out Waldmeister from default for now -- success rate too low on Judgment Day
2011-05-27, by blanchet
document relevance filter a bit more
2011-05-27, by blanchet
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
2011-05-27, by blanchet
towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
2011-05-27, by blanchet
instance inat for complete_lattice
2011-05-26, by noschinl
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)
2011-05-26, by boehmes
integral strong monotone; finite subadditivity for measure
2011-05-26, by hoelzl
composition of convex and measurable function is measurable
2011-05-26, by hoelzl
introduce independence of two random variables
2011-05-26, by hoelzl
add lemma indep_distribution_eq_measure
2011-05-26, by hoelzl
add lemma indep_rv_finite
2011-05-26, by hoelzl
generalize setsum_cases
2011-05-26, by hoelzl
add lemma borel_0_1_law
2011-05-26, by hoelzl
add lemma sigma_sets_singleton
2011-05-26, by hoelzl
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip