* Local theory targets ``context/locale/class ... begin'' followed by ``end''.

--- a/NEWS	Sat Nov 11 16:11:44 2006 +0100
+++ b/NEWS	Sat Nov 11 16:12:23 2006 +0100
@@ -35,6 +35,13 @@
 older versions of Isabelle will fail to start up if a negative prems
 limit is imposed.
 
+* Local theory targets may be specified by non-nested blocks of
+``context/locale/class ... begin'' followed by ``end''.  The body may
+contain definitions, theorems etc., including any derived mechanism
+that has been implemented on top of these primitives.  This concept
+generalizes the existing ``theorem (in ...)'' towards more versatility
+and scalability.
+
 
 *** Document preparation ***