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
-28
+28
+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.
imported patch sledge_doc_metis_as_prover
2011-05-30, by blanchet
automatically minimize with Metis when this can be done within a few seconds
2011-05-30, by blanchet
minimize with Metis if possible
2011-05-30, by blanchet
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
2011-05-30, by blanchet
Workaround for hyperref bug affecting index entries involving the | symbol
2011-05-30, by paulson
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
2011-05-30, by bulwahn
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
2011-05-30, by bulwahn
merged multiple heads
2011-05-30, by paulson
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
2011-05-30, by paulson
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
2011-05-29, by blanchet
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-28
+28
+50
+100
+300
+1000
+3000
+10000
+30000
tip