* Pure: locale specifications now produce predicate definitions;
authorwenzelm
Wed Jul 24 00:08:52 2002 +0200 (2002-07-24)
changeset 13410f2cd09766864
parent 13409 d4ea094c650e
child 13411 181a293aa37a
* Pure: locale specifications now produce predicate definitions;
NEWS
     1.1 --- a/NEWS	Tue Jul 23 15:07:12 2002 +0200
     1.2 +++ b/NEWS	Wed Jul 24 00:08:52 2002 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -6,6 +7,14 @@
     1.9  
    1.10  *** General ***
    1.11  
    1.12 +* Pure: locale specifications now produce predicate definitions
    1.13 +according to the body of text (covering assumptions modulo local
    1.14 +definitions); predicate "loc_axioms" covers newly introduced text,
    1.15 +while "loc" is cumulative wrt. all included locale expressions; the
    1.16 +latter view is presented only on export into the global theory
    1.17 +context; potential INCOMPATIBILITY, use "(open)" option to fall back
    1.18 +on the old view without predicates;
    1.19 +
    1.20  * improved thms_containing: proper indexing of facts instead of raw
    1.21  theorems; check validity of results wrt. current name space; include
    1.22  local facts of proof configuration (also covers active locales); an