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