Mon, 30 May 2011 17:00:38 +0200 better merging of similar outputs
blanchet [Mon, 30 May 2011 17:00:38 +0200] rev 43055
better merging of similar outputs
Mon, 30 May 2011 17:00:38 +0200 update minimization documentation
blanchet [Mon, 30 May 2011 17:00:38 +0200] rev 43054
update minimization documentation
Mon, 30 May 2011 17:00:38 +0200 imported patch sledge_doc_metis_as_prover
blanchet [Mon, 30 May 2011 17:00:38 +0200] rev 43053
imported patch sledge_doc_metis_as_prover
Mon, 30 May 2011 17:00:38 +0200 automatically minimize with Metis when this can be done within a few seconds
blanchet [Mon, 30 May 2011 17:00:38 +0200] rev 43052
automatically minimize with Metis when this can be done within a few seconds
Mon, 30 May 2011 17:00:38 +0200 minimize with Metis if possible
blanchet [Mon, 30 May 2011 17:00:38 +0200] rev 43051
minimize with Metis if possible
Mon, 30 May 2011 17:00:38 +0200 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet [Mon, 30 May 2011 17:00:38 +0200] rev 43050
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
Mon, 30 May 2011 15:30:05 +0100 Workaround for hyperref bug affecting index entries involving the | symbol
paulson [Mon, 30 May 2011 15:30:05 +0100] rev 43049
Workaround for hyperref bug affecting index entries involving the | symbol
Mon, 30 May 2011 13:58:00 +0200 improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn [Mon, 30 May 2011 13:58:00 +0200] rev 43048
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
Mon, 30 May 2011 13:57:59 +0200 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
bulwahn [Mon, 30 May 2011 13:57:59 +0200] rev 43047
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
Mon, 30 May 2011 12:20:04 +0100 merged multiple heads
paulson [Mon, 30 May 2011 12:20:04 +0100] rev 43046
merged multiple heads
Mon, 30 May 2011 12:15:17 +0100 Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
paulson [Mon, 30 May 2011 12:15:17 +0100] rev 43045
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
Sun, 29 May 2011 19:40:56 +0200 always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
blanchet [Sun, 29 May 2011 19:40:56 +0200] rev 43044
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
Sun, 29 May 2011 19:40:56 +0200 normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet [Sun, 29 May 2011 19:40:56 +0200] rev 43043
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
Fri, 27 May 2011 21:11:44 +0200 function tutorial: do not omit termination proof, even when discussing other things
krauss [Fri, 27 May 2011 21:11:44 +0200] rev 43042
function tutorial: do not omit termination proof, even when discussing other things
Fri, 27 May 2011 16:45:24 +0200 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
boehmes [Fri, 27 May 2011 16:45:24 +0200] rev 43041
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
Fri, 27 May 2011 10:41:09 +0200 document new "try"
blanchet [Fri, 27 May 2011 10:41:09 +0200] rev 43040
document new "try"
Fri, 27 May 2011 10:33:16 +0200 tuned comments
blanchet [Fri, 27 May 2011 10:33:16 +0200] rev 43039
tuned comments
Fri, 27 May 2011 10:30:08 +0200 new timeout section (cf. Nitpick manual)
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43038
new timeout section (cf. Nitpick manual)
Fri, 27 May 2011 10:30:08 +0200 cleanup proof text generation code
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43037
cleanup proof text generation code
Fri, 27 May 2011 10:30:08 +0200 more Sledgehammer documentation updates
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43036
more Sledgehammer documentation updates
Fri, 27 May 2011 10:30:08 +0200 minor update
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43035
minor update
Fri, 27 May 2011 10:30:08 +0200 try both "metis" and (on failure) "metisFT" in replay
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43034
try both "metis" and (on failure) "metisFT" in replay
Fri, 27 May 2011 10:30:08 +0200 show time taken for reconstruction
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43033
show time taken for reconstruction
Fri, 27 May 2011 10:30:08 +0200 unbreak "max_potential" logic
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43032
unbreak "max_potential" logic
Fri, 27 May 2011 10:30:08 +0200 more concise output
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43031
more concise output
Fri, 27 May 2011 10:30:08 +0200 compile
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43030
compile
Fri, 27 May 2011 10:30:08 +0200 use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43029
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
Fri, 27 May 2011 10:30:08 +0200 repaired theory merging and defined/used helpers
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43028
repaired theory merging and defined/used helpers
Fri, 27 May 2011 10:30:08 +0200 make Sledgehammer a little bit less verbose in "try"
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43027
make Sledgehammer a little bit less verbose in "try"
Fri, 27 May 2011 10:30:08 +0200 handle non-auto try cases gracefully in Try Methods
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43026
handle non-auto try cases gracefully in Try Methods
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip