* Pure/library: divide_and_conquer;
* Theory Real: new method ferrack;

--- a/NEWS	Tue May 16 18:20:26 2006 +0200
+++ b/NEWS	Tue May 16 18:31:46 2006 +0200
@@ -428,6 +428,14 @@
 association lists.
 
 
+*** HOL-Complex ***
+
+* Theory Real: new method ferrack implements quantifier elimination
+for linear arithmetic over the reals. The quantifier elimination
+feature is used only for decision, for compatibility with arith. This
+means a goal is either solved or left unchanged, no simplification.
+
+
 *** ML ***
 
 * Pure/library:
@@ -463,6 +471,8 @@
 Note that fold_index starts counting at index 0, not 1 like foldln
 used to.
 
+* Pure/library: general ``divide_and_conquer'' combinator on lists.
+
 * Pure/General/name_mangler.ML provides a functor for generic name
 mangling (bijective mapping from any expression values to strings).