NEWS
changeset 24086 21900a460ba4
parent 24032 b3d7eb6f535f
child 24110 4ab3084e311c
     1.1 --- a/NEWS	Tue Jul 31 13:30:35 2007 +0200
     1.2 +++ b/NEWS	Tue Jul 31 13:31:01 2007 +0200
     1.3 @@ -161,6 +161,23 @@
     1.4  Command 'print_theory' outputs the normalized system of recursive
     1.5  equations, see section "definitions".
     1.6  
     1.7 +* Configuration options are maintained within the theory or proof
     1.8 +context (with name and type bool/int/string), providing a very simple
     1.9 +interface to a poor-man's version of general context data.  Tools may
    1.10 +declare options in ML (e.g. using ConfigOption.int) and then refer to
    1.11 +these values using ConfigOption.get etc.  Users may change options via
    1.12 +the "option" attribute, which works particularly well with commands
    1.13 +'declare' or 'using', for example ``declare [[option foo = 42]]''.
    1.14 +Thus global reference variables are easily avoided, which do not
    1.15 +observe Isar toplevel undo/redo and fail to work with multithreading.
    1.16 +
    1.17 +* Named collections of theorems may be easily installed as context
    1.18 +data using the functor NamedThmsFun (see
    1.19 +src/Pure/Tools/named_thms.ML).  The user may add or delete facts via
    1.20 +attributes.  This is just a common case of general context data, which
    1.21 +is the preferred way for anything more complex than just a list of
    1.22 +facts in canonical order.
    1.23 +
    1.24  * Isar: command 'declaration' augments a local theory by generic
    1.25  declaration functions written in ML.  This enables arbitrary content
    1.26  being added to the context, depending on a morphism that tells the