| changeset 17445 | 3c9c46b820f5 |
| parent 17442 | c0f0b92c198c |
| child 17457 | 5b9538fc6d67 |
--- a/NEWS Sat Sep 17 11:49:29 2005 +0200 +++ b/NEWS Sat Sep 17 12:18:00 2005 +0200 @@ -673,6 +673,12 @@ the old version is still required for ML proof scripts. +*** Cube *** + +* Converted to Isar theory format; use locales instead of axiomatic +theories. + + *** ML *** * Pure/library.ML no longer defines its own option datatype, but uses