| changeset 5722 | c669e2161b08 |
| parent 5710 | 30f4d3713cbe |
| child 5726 | 5de7e399ec88 |
--- 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