locales
authorpaulson
Thu Oct 22 10:57:18 1998 +0200 (1998-10-22)
changeset 5722c669e2161b08
parent 5721 458a67fd5461
child 5723 81e1a83ee002
locales
NEWS
     1.1 --- a/NEWS	Wed Oct 21 17:57:02 1998 +0200
     1.2 +++ b/NEWS	Thu Oct 22 10:57:18 1998 +0200
     1.3 @@ -105,6 +105,9 @@
     1.4  * new top-level commands 'thm' and 'thms' for retrieving theorems from
     1.5  the current theory context, and 'theory' to lookup stored theories;
     1.6  
     1.7 +* new theory section 'locale' for declaring constants, assumptions and
     1.8 +definitions that have local scope;
     1.9 +
    1.10  * new theory section 'nonterminals' for purely syntactic types;
    1.11  
    1.12  * new theory section 'setup' for generic ML setup functions