1.1 --- a/NEWS	Tue Oct 28 11:03:07 2008 +0100
     1.2 +++ b/NEWS	Tue Oct 28 11:05:44 2008 +0100
     1.3 @@ -206,6 +206,9 @@
     1.4  * The metis method now fails in the usual manner, rather than raising
     1.5  an exception, if it determines that it cannot prove the theorem.
     1.6  
     1.7 +* The metis method no longer fails because the theorem is too trivial
     1.8 +(contains the empty clause).
     1.9 +
    1.10  * Methods "case_tac" and "induct_tac" now refer to the very same rules
    1.11  as the structured Isar versions "cases" and "induct", cf. the
    1.12  corresponding "cases" and "induct" attributes.  Mutual induction rules