NEWS
changeset 22863 e1d3fa78b8e1
parent 22848 f65a76867179
child 22871 9ffb43b19ec6
     1.1 --- a/NEWS	Tue May 08 08:21:39 2007 +0200
     1.2 +++ b/NEWS	Tue May 08 15:01:28 2007 +0200
     1.3 @@ -903,8 +903,9 @@
     1.4  *** ML ***
     1.5  
     1.6  * Context data interfaces (Theory/Proof/GenericDataFun): removed
     1.7 -name/print, use adhoc value for uninitialized data, init only required
     1.8 -for impure data.
     1.9 +name/print, uninitialized data defaults to ad-hoc copy of empty value,
    1.10 +init only required for impure data.  INCOMPATIBILITY: empty really
    1.11 +need to be empty (no dependencies on theory content!)
    1.12  
    1.13  * ML within Isar: antiquotations allow to embed statically-checked
    1.14  formal entities in the source, referring to the context available at