# HG changeset patch
# User wenzelm
# Date 1147797106 -7200
# Node ID 39c37e16f748e5be5edc21db18b5b2d35e40d110
# Parent  f0594a06f2f058688695b10430a870c6af965185
* Pure/library: divide_and_conquer;
* Theory Real: new method ferrack;

diff -r f0594a06f2f0 -r 39c37e16f748 NEWS
--- 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).