* HOL-Statespace;
authorwenzelm
Sun Nov 11 16:45:47 2007 +0100 (2007-11-11)
changeset 2539782deaaba928d
parent 25396 e7ddcf8bcf9a
child 25398 35f600d9bf06
* HOL-Statespace;
NEWS
     1.1 --- a/NEWS	Sun Nov 11 16:24:22 2007 +0100
     1.2 +++ b/NEWS	Sun Nov 11 16:45:47 2007 +0100
     1.3 @@ -1122,6 +1122,13 @@
     1.4  * Reflection: Automatic reification now handels binding, an example is
     1.5  available in src/HOL/ex/ReflectionEx.thy
     1.6  
     1.7 +* HOL-Statespace: ``State Spaces: The Locale Way'' introduces a
     1.8 +command 'statespace' that is simular to 'record', but introduces an
     1.9 +abstract specification based on the locale infrastructure instead of
    1.10 +HOL types.  This leads to extra flexibility in composing state spaces,
    1.11 +in particular multiple inheritance and renaming of components.
    1.12 +
    1.13 +
    1.14  
    1.15  *** HOL-Complex ***
    1.16