# HG changeset patch
# User wenzelm
# Date 1027462132 -7200
# Node ID f2cd097668646ca5f60a40412a518383b6cac847
# Parent  d4ea094c650ed7e2cfe81ffbbd3c5f58ecc4847e
* Pure: locale specifications now produce predicate definitions;

diff -r d4ea094c650e -r f2cd09766864 NEWS
--- a/NEWS	Tue Jul 23 15:07:12 2002 +0200
+++ b/NEWS	Wed Jul 24 00:08:52 2002 +0200
@@ -1,3 +1,4 @@
+
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -6,6 +7,14 @@
 
 *** General ***
 
+* Pure: locale specifications now produce predicate definitions
+according to the body of text (covering assumptions modulo local
+definitions); predicate "loc_axioms" covers newly introduced text,
+while "loc" is cumulative wrt. all included locale expressions; the
+latter view is presented only on export into the global theory
+context; potential INCOMPATIBILITY, use "(open)" option to fall back
+on the old view without predicates;
+
 * improved thms_containing: proper indexing of facts instead of raw
 theorems; check validity of results wrt. current name space; include
 local facts of proof configuration (also covers active locales); an