[isabelle-dev] NEWS

[Makarius]

* 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.

* 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.