--- a/NEWS Mon Apr 07 15:37:04 2008 +0200
+++ b/NEWS Mon Apr 07 15:37:27 2008 +0200
@@ -173,6 +173,8 @@
* Metis prover is now an order of magnitude faster, and also works
with multithreading.
+* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
+
* Sledgehammer no longer produces structured proofs by default. To enable,
declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus,
reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts.