Fri, 27 May 2011 16:45:24 +0200added 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 43882
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 +0200document new "try"
blanchet [Fri, 27 May 2011 10:41:09 +0200] rev 43881
document new "try"

Fri, 27 May 2011 10:33:16 +0200tuned comments
blanchet [Fri, 27 May 2011 10:33:16 +0200] rev 43880
tuned comments

Fri, 27 May 2011 10:30:08 +0200new timeout section (cf. Nitpick manual)
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43879
new timeout section (cf. Nitpick manual)

Fri, 27 May 2011 10:30:08 +0200cleanup proof text generation code
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43878
cleanup proof text generation code

Fri, 27 May 2011 10:30:08 +0200more Sledgehammer documentation updates
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43877
more Sledgehammer documentation updates

Fri, 27 May 2011 10:30:08 +0200minor update
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43876
minor update

Fri, 27 May 2011 10:30:08 +0200try both "metis" and (on failure) "metisFT" in replay
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43875
try both "metis" and (on failure) "metisFT" in replay

Fri, 27 May 2011 10:30:08 +0200show time taken for reconstruction
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43874
show time taken for reconstruction

Fri, 27 May 2011 10:30:08 +0200unbreak "max_potential" logic
blanchet [Fri, 27 May 2011 10:30:08 +0200] rev 43873
unbreak "max_potential" logic