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
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.
added appropriate method for skolemization of Z3 steps to the mix
2014-08-01, by blanchet
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
2014-08-01, by blanchet
honor 'try0' also for one-liners
2014-08-01, by blanchet
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
2014-08-01, by blanchet
further minimize one-liner
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
eliminated needlessly complex message tail
2014-08-01, by blanchet
updated NEWS
2014-08-01, by blanchet
update documentation after removal of 'min' subcommand
2014-08-01, by blanchet
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-08-01, by blanchet
rationalized preplaying by eliminating (now superfluous) laziness
2014-08-01, by blanchet
removed proof methods as provers from docs
2014-08-01, by blanchet
simplified minimization logic
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
remove lambda-lifting related assumptions from generated Isar proofs
2014-08-01, by blanchet
whitespace tuning
2014-08-01, by blanchet
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
2014-08-01, by blanchet
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
2014-08-01, by blanchet
simplified tactics slightly
2014-07-31, by traytel
cascading timeout in parallel evaluation, to rapidly find optimum
2014-07-31, by blanchet
put faster proof methods first
2014-07-30, by blanchet
use parallel preplay machinery also for one-line proofs
2014-07-30, by blanchet
updated docs
2014-07-30, by blanchet
always minimize Sledgehammer results by default
2014-07-30, by blanchet
tuned ML function name
2014-07-30, by blanchet
reduced preplay timeout to 1 s
2014-07-30, by blanchet
added more proof methods for one-liners
2014-07-30, by blanchet
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
2014-07-30, by blanchet
Improving robustness and indentation corrections.
2014-07-30, by fleury
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
2014-07-30, by fleury
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
tip