--- a/NEWS Sun Aug 28 16:04:49 2005 +0200
+++ b/NEWS Sun Aug 28 16:04:50 2005 +0200
@@ -19,7 +19,7 @@
will disappear in the next release. Use isatool fixheaders to convert
existing theory files. Note that there is no change in ancient
-non-Isar theories.
+non-Isar theories now, but these are likely to disappear soon.
* Theory loader: parent theories can now also be referred to via
relative and absolute paths.
@@ -659,6 +659,11 @@
provides a clean interface for unusual systems where the internal and
external process view of file names are different.
+* ML functions legacy_bindings and use_legacy_bindings produce ML fact
+bindings for all theorems stored within a given theory; this may help
+in porting non-Isar theories to Isar ones, while keeping ML proof
+scripts for the time being.
+
*** System ***