Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+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.
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip