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
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
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
krauss [Fri, 27 May 2011 21:11:44 +0200] rev 43042
function tutorial: do not omit termination proof, even when discussing other things
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
blanchet [Fri, 27 May 2011 10:41:09 +0200] rev 43040
document new "try"
blanchet [Fri, 27 May 2011 10:33:16 +0200] rev 43039
tuned comments
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43038
new timeout section (cf. Nitpick manual)
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43037
cleanup proof text generation code
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43036
more Sledgehammer documentation updates
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43035
minor update
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43034
try both "metis" and (on failure) "metisFT" in replay
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43033
show time taken for reconstruction
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43032
unbreak "max_potential" logic
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43031
more concise output
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43030
compile
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)
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43028
repaired theory merging and defined/used helpers
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43027
make Sledgehammer a little bit less verbose in "try"
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43026
handle non-auto try cases gracefully in Try Methods
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43025
handle non-auto try case gracefully in Solve Direct
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43024
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43023
update SML section of documentation
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43022
handle non-auto try case gracefully in Nitpick
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43021
handle non-auto try case of Sledgehammer better
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43020
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43019
removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43018
renamed "Auto_Tools" "Try"
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43017
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43016
renamed "try" "try_methods"