--- a/NEWS Wed Apr 14 22:18:10 2010 +0200
+++ b/NEWS Thu Apr 15 12:27:14 2010 +0200
@@ -74,6 +74,8 @@
*** Pure ***
+* Code generator: simple concept for abstract datatypes obeying invariants.
+
* Local theory specifications may depend on extra type variables that
are not present in the result type -- arguments TYPE('a) :: 'a itself
are added internally. For example:
@@ -106,6 +108,10 @@
*** HOL ***
+* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
+provides abstract red-black tree type which is backed by RBT_Impl
+as implementation. INCOMPATIBILTY.
+
* Command 'typedef' now works within a local theory context -- without
introducing dependencies on parameters or assumptions, which is not
possible in Isabelle/Pure/HOL. Note that the logical environment may