# HG changeset patch
# User krauss
# Date 1193401472 -7200
# Node ID 1e904070e9cbf42c53c84d5af977f7572cad57d2
# Parent  7a169cfda8664e7d35b74140b2557b26edf6028b
added NEWS entry for function package

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