--- a/NEWS Tue Sep 16 12:24:37 2008 +0200
+++ b/NEWS Tue Sep 16 12:25:04 2008 +0200
@@ -130,6 +130,9 @@
(instead of Main), thus theory Main occasionally has to be imported
explicitly.
+* The metis method now fails in the usual manner, rather than raising an exception,
+if it determines that it cannot prove the theorem.
+
* Methods "case_tac" and "induct_tac" now refer to the very same rules
as the structured Isar versions "cases" and "induct", cf. the
corresponding "cases" and "induct" attributes. Mutual induction rules