Mon, 30 May 2011 17:00:38 +0200 blanchet better merging of similar outputs
Mon, 30 May 2011 17:00:38 +0200 blanchet update minimization documentation
Mon, 30 May 2011 17:00:38 +0200 blanchet imported patch sledge_doc_metis_as_prover
Mon, 30 May 2011 17:00:38 +0200 blanchet automatically minimize with Metis when this can be done within a few seconds
Mon, 30 May 2011 17:00:38 +0200 blanchet minimize with Metis if possible
Mon, 30 May 2011 17:00:38 +0200 blanchet support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
Mon, 30 May 2011 15:30:05 +0100 paulson Workaround for hyperref bug affecting index entries involving the | symbol
Mon, 30 May 2011 13:58:00 +0200 bulwahn 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 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
Mon, 30 May 2011 12:20:04 +0100 paulson merged multiple heads
Mon, 30 May 2011 12:15:17 +0100 paulson Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
Sun, 29 May 2011 19:40:56 +0200 blanchet 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 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
Fri, 27 May 2011 21:11:44 +0200 krauss function tutorial: do not omit termination proof, even when discussing other things
Fri, 27 May 2011 16:45:24 +0200 boehmes 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 blanchet document new "try"
Fri, 27 May 2011 10:33:16 +0200 blanchet tuned comments
Fri, 27 May 2011 10:30:08 +0200 blanchet new timeout section (cf. Nitpick manual)
Fri, 27 May 2011 10:30:08 +0200 blanchet cleanup proof text generation code
Fri, 27 May 2011 10:30:08 +0200 blanchet more Sledgehammer documentation updates
Fri, 27 May 2011 10:30:08 +0200 blanchet minor update
Fri, 27 May 2011 10:30:08 +0200 blanchet try both "metis" and (on failure) "metisFT" in replay
Fri, 27 May 2011 10:30:08 +0200 blanchet show time taken for reconstruction
Fri, 27 May 2011 10:30:08 +0200 blanchet unbreak "max_potential" logic
Fri, 27 May 2011 10:30:08 +0200 blanchet more concise output
Fri, 27 May 2011 10:30:08 +0200 blanchet compile
Fri, 27 May 2011 10:30:08 +0200 blanchet 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 blanchet repaired theory merging and defined/used helpers
Fri, 27 May 2011 10:30:08 +0200 blanchet make Sledgehammer a little bit less verbose in "try"
Fri, 27 May 2011 10:30:08 +0200 blanchet 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