| changeset 22848 | f65a76867179 |
| parent 22845 | 5f9138bcb3d7 |
| child 22863 | e1d3fa78b8e1 |
--- a/NEWS Mon May 07 00:50:09 2007 +0200 +++ b/NEWS Mon May 07 00:52:25 2007 +0200 @@ -902,6 +902,10 @@ *** ML *** +* Context data interfaces (Theory/Proof/GenericDataFun): removed +name/print, use adhoc value for uninitialized data, init only required +for impure data. + * ML within Isar: antiquotations allow to embed statically-checked formal entities in the source, referring to the context available at compile-time. For example: