NEWS

--- a/NEWS	Tue Mar 09 23:29:04 2010 +0100
+++ b/NEWS	Tue Mar 09 23:32:13 2010 +0100
@@ -76,6 +76,10 @@
 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.
+
 
 *** HOL ***