1.1 --- a/NEWS	Fri Oct 26 10:32:10 2007 +0200
     1.2 +++ b/NEWS	Fri Oct 26 14:24:32 2007 +0200
     1.3 @@ -912,6 +912,16 @@
     1.4      sets or predicates are now called "p_1.cases" ... "p_k.cases". The
     1.5      list of rules "p_1_..._p_k.elims" is no longer available.
     1.6  
     1.7 +* New package "function"/"fun" for general recursive functions,
     1.8 +supporting mutual and nested recursion, definitions in local contexts,
     1.9 +more general pattern matching and partiality. See HOL/ex/Fundefs.thy
    1.10 +for small examples, and the separate tutorial on the function
    1.11 +package. The old recdef "package" is still available as before, but
    1.12 +users are encouraged to use the new package.
    1.13 +
    1.14 +* Method "lexicographic_order" automatically synthesizes termination
    1.15 +relations as lexicographic combinations of size measures. 
    1.16 +
    1.17  * Case-expressions allow arbitrary constructor-patterns (including
    1.18  "_") and take their order into account, like in functional
    1.19  programming.  Internally, this is translated into nested
    1.20 @@ -989,10 +999,6 @@
    1.21  * Dropped redundant lemma if_def2 in favor of if_bool_eq_conj.
    1.22  INCOMPATIBILITY.
    1.23  
    1.24 -* Method "lexicographic_order" automatically synthesizes termination
    1.25 -relations as lexicographic combinations of size measures -- 'function'
    1.26 -package.
    1.27 -
    1.28  * HOL/records: generalised field-update to take a function on the
    1.29  field rather than the new value: r(|A := x|) is translated to A_update
    1.30  (K x) r The K-combinator that is internally used is called K_record.