# HG changeset patch
# User wenzelm
# Date 1194795947 -3600
# Node ID 82deaaba928d920c2b1e5302bd9a329448cf58ca
# Parent  e7ddcf8bcf9a2b6dd810819f089a3c068f235292
* HOL-Statespace;

diff -r e7ddcf8bcf9a -r 82deaaba928d NEWS
--- a/NEWS	Sun Nov 11 16:24:22 2007 +0100
+++ b/NEWS	Sun Nov 11 16:45:47 2007 +0100
@@ -1122,6 +1122,13 @@
 * Reflection: Automatic reification now handels binding, an example is
 available in src/HOL/ex/ReflectionEx.thy
 
+* HOL-Statespace: ``State Spaces: The Locale Way'' introduces a
+command 'statespace' that is simular to 'record', but introduces an
+abstract specification based on the locale infrastructure instead of
+HOL types.  This leads to extra flexibility in composing state spaces,
+in particular multiple inheritance and renaming of components.
+
+
 
 *** HOL-Complex ***