--- a/NEWS Fri Mar 20 17:04:44 2009 +0100
+++ b/NEWS Fri Mar 20 17:12:37 2009 +0100
@@ -685,6 +685,12 @@
Syntax.read_term_global etc.; see also OldGoals.read_term as last
resort for legacy applications.
+* Disposed old declarations, tactics, tactic combinators that refer to
+the simpset or claset of an implicit theory (such as Addsimps,
+Simp_tac, SIMPSET). INCOMPATIBILITY, should use @{simpset} etc. in
+embedded ML text, or local_simpset_of with a proper context passed as
+explicit runtime argument.
+
* Antiquotations: block-structured compilation context indicated by
\<lbrace> ... \<rbrace>; additional antiquotation forms: