diff -r eaf634e975fa -r 73efc70edeef NEWS
--- a/NEWS	Tue Mar 18 22:19:18 2008 +0100
+++ b/NEWS	Tue Mar 18 23:25:06 2008 +0100
@@ -22,6 +22,10 @@
 conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which
 provides a proper context already.
 
+* Theory loader: old-style ML proof scripts being *attached* to a thy
+file are no longer supported.  INCOMPATIBILITY, regular 'uses' and
+'use' within a theory file will do the job.
+
 
 *** Pure ***
 
@@ -44,7 +48,7 @@
 redundant lemmas less_trans, less_linear, le_imp_less_or_eq,
 le_less_trans, less_le_trans, which merely duplicate lemmas of the
 same name in theory Orderings.  Potential INCOMPATIBILITY due to more
-general and different variable names.
+general types and different variable names.
 
 * Library/Option_ord.thy: Canonical order on option type.