blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43850
reintroduced Waldmeister but limit the number of remote threads created
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43849
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43848
minor doc adjustments
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43847
make output more concise
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43846
merge timeout messages from several ATPs into one message to avoid clutter
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43845
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43844
tuning
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43843
mention contributions from LCP and explain metis and metisFT encodings
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43842
fixed trivial fact detection
blanchet [Fri, 27 May 2011 10:30:07 +0200] rev 43841
cleaner handling of equality and proxies (esp. for THF)