# HG changeset patch
# User wenzelm
# Date 1210967773 -7200
# Node ID ce964f0df281237994a175a1321c3d1e215013a4
# Parent  485213276a2a9af7de3cc1d8162c99897cfd6663
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
* Isar statements: removed obsolete case "rule_context";

diff -r 485213276a2a -r ce964f0df281 NEWS
--- 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.