--- a/NEWS Wed Aug 01 16:50:16 2007 +0200
+++ b/NEWS Wed Aug 01 16:55:37 2007 +0200
@@ -164,19 +164,21 @@
* Configuration options are maintained within the theory or proof
context (with name and type bool/int/string), providing a very simple
interface to a poor-man's version of general context data. Tools may
-declare options in ML (e.g. using ConfigOption.int) and then refer to
-these values using ConfigOption.get etc. Users may change options via
-the "option" attribute, which works particularly well with commands
-'declare' or 'using', for example ``declare [[option foo = 42]]''.
-Thus global reference variables are easily avoided, which do not
-observe Isar toplevel undo/redo and fail to work with multithreading.
+declare options in ML (e.g. using Attrib.config_int) and then refer to
+these values using Config.get etc. Users may change options via an
+associated attribute of the same name. This form of context
+declaration works particularly well with commands 'declare' or
+'using', for example ``declare [[foo = 42]]''. Thus it has become
+very easy to avoid global references, which would not observe Isar
+toplevel undo/redo and fail to work with multithreading.
* Named collections of theorems may be easily installed as context
data using the functor NamedThmsFun (see
src/Pure/Tools/named_thms.ML). The user may add or delete facts via
-attributes. This is just a common case of general context data, which
-is the preferred way for anything more complex than just a list of
-facts in canonical order.
+attributes; there is also a toplevel print command. This facility is
+just a common case of general context data, which is the preferred way
+for anything more complex than just a list of facts in canonical
+order.
* Isar: command 'declaration' augments a local theory by generic
declaration functions written in ML. This enables arbitrary content