* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
* Isar statements: removed obsolete case "rule_context";

--- a/NEWS	Fri May 16 21:53:30 2008 +0200
+++ b/NEWS	Fri May 16 21:56:13 2008 +0200
@@ -97,6 +97,13 @@
 "fact".  INCOMPATIBILITY: need to name facts explicitly in rare
 situations.
 
+* Method "cases", "induct", "coinduct": removed obsolete/undocumented
+"(open)" option, which used to expose internal bound variables to the
+proof text.
+
+* Isar statements: removed obsolete case "rule_context".
+INCOMPATIBILITY, better use explicit fixes/assumes.
+
 * Locale proofs: default proof step now includes 'unfold_locales';
 hence 'proof' without argument may be used to unfold locale
 predicates.