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) -------------------------------------