NEWS
changeset 54449 f3cfe882f9af
parent 54384 50199af40c27
child 54489 03ff4d1e6784
--- a/NEWS	Sat Nov 16 17:04:17 2013 +0100
+++ b/NEWS	Sat Nov 16 17:39:11 2013 +0100
@@ -62,6 +62,15 @@
 instead of explicitly stating boundedness of sets.
 
 
+*** ML ***
+
+* Toplevel function "use" refers to raw ML bootstrap environment,
+without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
+Note that 'ML_file' is the canonical command to load ML files into the
+formal context.
+
+
+
 New in Isabelle2013-1 (November 2013)
 -------------------------------------