| changeset 26401 | e7a94081dce7 |
| parent 26387 | 7807cbf7640f |
| child 26422 | d5883907c514 |
--- a/NEWS Tue Mar 25 21:59:48 2008 +0100 +++ b/NEWS Tue Mar 25 22:12:02 2008 +0100 @@ -172,6 +172,9 @@ *** ML *** +* Functor NamedThmsFun: data is available to the user as dynamic fact +(of the same name). + * Removed obsolete "use_legacy_bindings" function. INCOMPATIBILITY. * ML within Isar: antiquotation @{const name} or @{const