locales

--- a/NEWS	Wed Oct 21 17:57:02 1998 +0200
+++ b/NEWS	Thu Oct 22 10:57:18 1998 +0200
@@ -105,6 +105,9 @@
 * new top-level commands 'thm' and 'thms' for retrieving theorems from
 the current theory context, and 'theory' to lookup stored theories;
 
+* new theory section 'locale' for declaring constants, assumptions and
+definitions that have local scope;
+
 * new theory section 'nonterminals' for purely syntactic types;
 
 * new theory section 'setup' for generic ML setup functions