NEWS
changeset 24110 4ab3084e311c
parent 24086 21900a460ba4
child 24172 06e42cf7df4e
     1.1 --- a/NEWS	Wed Aug 01 16:50:16 2007 +0200
     1.2 +++ b/NEWS	Wed Aug 01 16:55:37 2007 +0200
     1.3 @@ -164,19 +164,21 @@
     1.4  * Configuration options are maintained within the theory or proof
     1.5  context (with name and type bool/int/string), providing a very simple
     1.6  interface to a poor-man's version of general context data.  Tools may
     1.7 -declare options in ML (e.g. using ConfigOption.int) and then refer to
     1.8 -these values using ConfigOption.get etc.  Users may change options via
     1.9 -the "option" attribute, which works particularly well with commands
    1.10 -'declare' or 'using', for example ``declare [[option foo = 42]]''.
    1.11 -Thus global reference variables are easily avoided, which do not
    1.12 -observe Isar toplevel undo/redo and fail to work with multithreading.
    1.13 +declare options in ML (e.g. using Attrib.config_int) and then refer to
    1.14 +these values using Config.get etc.  Users may change options via an
    1.15 +associated attribute of the same name.  This form of context
    1.16 +declaration works particularly well with commands 'declare' or
    1.17 +'using', for example ``declare [[foo = 42]]''.  Thus it has become
    1.18 +very easy to avoid global references, which would not observe Isar
    1.19 +toplevel undo/redo and fail to work with multithreading.
    1.20  
    1.21  * Named collections of theorems may be easily installed as context
    1.22  data using the functor NamedThmsFun (see
    1.23  src/Pure/Tools/named_thms.ML).  The user may add or delete facts via
    1.24 -attributes.  This is just a common case of general context data, which
    1.25 -is the preferred way for anything more complex than just a list of
    1.26 -facts in canonical order.
    1.27 +attributes; there is also a toplevel print command.  This facility is
    1.28 +just a common case of general context data, which is the preferred way
    1.29 +for anything more complex than just a list of facts in canonical
    1.30 +order.
    1.31  
    1.32  * Isar: command 'declaration' augments a local theory by generic
    1.33  declaration functions written in ML.  This enables arbitrary content