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.
more robust and simpler adjustment computation
2011-05-31, by blanchet
more work on new Metis
2011-05-31, by blanchet
tuning
2011-05-31, by blanchet
more work on new metis that exploits the powerful new type encodings
2011-05-31, by blanchet
tuning
2011-05-31, by blanchet
removed obscure option
2011-05-31, by blanchet
added "metisX" syntax (temporary)
2011-05-31, by blanchet
compile
2011-05-31, by blanchet
added new metis mode, with no implementation yet
2011-05-31, by blanchet
tuning
2011-05-31, by blanchet
first step in sharing more code between ATP and Metis translation
2011-05-31, by blanchet
more precise authorship, reflecting my own ignorance and hg annotate
2011-05-31, by krauss
generate raw induction rule as instance of generic rule with careful treatment of currying
2011-05-31, by krauss
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
2011-05-31, by krauss
admissibility on option type
2011-05-31, by krauss
also manage induction rule;
2011-05-23, by krauss
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
2011-05-30, by bulwahn
merged
2011-05-30, by paulson
Workaround for bug involving makeindex, hyperref and the | symbol
2011-05-30, by paulson
parameterize print_theorems over actual search function
2011-05-30, by krauss
added experimental yxml_find_theorems web service (but no client yet)
2011-05-30, by krauss
generic ScgiServer.simple_handler
2011-05-30, by krauss
moved html templates to a separate module, making their awkward signatures explicit
2011-05-30, by krauss
attempt to clarify code; removed "handle _" and dead code
2011-05-30, by krauss
(de)serialization for search query and result
2011-05-30, by krauss
explicit type for search queries
2011-05-30, by krauss
moved questionable goal modification out of filter_theorems
2011-05-30, by krauss
exported raw query parser; removed inconsistent clone
2011-05-30, by krauss
separate query parsing from actual search
2011-05-30, by krauss
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
2011-05-30, by blanchet
document new explicit apply
2011-05-30, by blanchet
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
2011-05-30, by blanchet
don't slice if there are too few facts
2011-05-30, by blanchet
nicer failure message when one-line proof reconstruction fails
2011-05-30, by blanchet
make SML/NJ happy
2011-05-30, by blanchet
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
2011-05-30, by blanchet
make all messages urgent in verbose mode
2011-05-30, by blanchet
minimize automatically even if Metis failed, if the external prover was really fast
2011-05-30, by blanchet
fixed syntax of min options
2011-05-30, by blanchet
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
2011-05-30, by blanchet
better merging of similar outputs
2011-05-30, by blanchet
update minimization documentation
2011-05-30, by blanchet
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip