diff -r 445e5a3244cc -r 965537d86fcc NEWS
--- a/NEWS	Thu Jul 22 20:46:45 2010 +0200
+++ b/NEWS	Thu Jul 22 22:31:20 2010 +0200
@@ -14,6 +14,11 @@
 consistent view on symbols, while raw explode (or String.explode)
 merely give a byte-oriented representation.
 
+* Special treatment of ML file names has been discontinued.
+Historically, optional extensions .ML or .sml were added on demand --
+at the cost of clarity of file dependencies.  Recall that Isabelle/ML
+files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
+
 
 *** HOL ***