# HG changeset patch
# User wenzelm
# Date 1163257943 -3600
# Node ID 73883a528b26a4d725c19328444f83a438779e49
# Parent  c432585af03b592e2d880ea52b47dad824f3eb33
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.

diff -r c432585af03b -r 73883a528b26 NEWS
--- 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 ***