# HG changeset patch
# User wenzelm
# Date 1126952280 -7200
# Node ID 3c9c46b820f5ea2302e9e0d79223ae835414d7ae
# Parent  a389e5892691fee27bc1975ed217746e51d20d5f
Cube: converted to Isar, use locales;

diff -r a389e5892691 -r 3c9c46b820f5 NEWS
--- 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