--- a/NEWS Fri May 13 16:03:03 2011 +0200
+++ b/NEWS Fri May 13 22:55:00 2011 +0200
@@ -144,6 +144,14 @@
* Slightly more special eq_list/eq_set, with shortcut involving
pointer equality (assumes that eq relation is reflexive).
+* Classical tactics use proper Proof.context instead of historic types
+claset/clasimpset. Old-style declarations like addIs, addEs, addDs
+operate directly on Proof.context. Raw type claset retains its use as
+snapshot of the classical context, which can be recovered via
+(put_claset HOL_cs) etc. Type clasimpset has been discontinued.
+INCOMPATIBILITY, classical tactics and derived proof methods require
+proper Proof.context.
+
New in Isabelle2011 (January 2011)