blanchet [Mon, 27 Jun 2011 14:56:35 +0200] rev 44439
clarify minimizer output
blanchet [Mon, 27 Jun 2011 14:56:33 +0200] rev 44438
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet [Mon, 27 Jun 2011 14:56:32 +0200] rev 44437
tweaked comment
blanchet [Mon, 27 Jun 2011 14:56:31 +0200] rev 44436
document "sound" option
blanchet [Mon, 27 Jun 2011 14:56:29 +0200] rev 44435
minor Sledgehammer news
blanchet [Mon, 27 Jun 2011 14:56:28 +0200] rev 44434
added "sound" option to force Sledgehammer to be pedantically sound
blanchet [Mon, 27 Jun 2011 14:56:26 +0200] rev 44433
removed "full_types" option from documentation
blanchet [Mon, 27 Jun 2011 14:56:10 +0200] rev 44432
document changes to Sledgehammer and "try"
blanchet [Mon, 27 Jun 2011 13:52:47 +0200] rev 44431
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet [Mon, 27 Jun 2011 13:52:47 +0200] rev 44430
clarify warning message to avoid confusing beginners