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