--- a/NEWS Mon Sep 06 21:33:19 2010 +0200
+++ b/NEWS Mon Sep 06 22:08:49 2010 +0200
@@ -232,6 +232,10 @@
* Configuration option show_question_marks only affects regular pretty
printing of types and terms, not raw Term.string_of_vname.
+* ML_Context.thm and ML_Context.thms are no longer pervasive. Rare
+INCOMPATIBILITY, superseded by static antiquotations @{thm} and
+@{thms} for most purposes.
+
* ML structure Unsynchronized never opened, not even in Isar
interaction mode as before. Old Unsynchronized.set etc. have been
discontinued -- use plain := instead. This should be *rare* anyway,