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