# 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.