--- a/NEWS Fri Apr 16 22:15:09 2010 +0200
+++ b/NEWS Fri Apr 16 22:18:59 2010 +0200
@@ -101,9 +101,9 @@
within a local theory context, with explicit checking of the
constructors involved (in contrast to the raw 'syntax' versions).
-* Command 'typedecl' now works within a local theory context --
-without introducing dependencies on parameters or assumptions, which
-is not possible in Isabelle/Pure.
+* Commands 'types' and 'typedecl' now work within a local theory
+context -- without introducing dependencies on parameters or
+assumptions, which is not possible in Isabelle/Pure.
* Proof terms: Type substitutions on proof constants now use canonical
order of type variables. INCOMPATIBILITY: Tools working with proof