--- 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