Cube: converted to Isar, use locales;

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