--- a/NEWS Mon Oct 15 01:57:50 2007 +0200
+++ b/NEWS Mon Oct 15 11:59:19 2007 +0200
@@ -732,6 +732,12 @@
CALCULEMUS 2007 for the general principles underlying this
architecture of context-aware proof-tools.
+* Method "ferrack" implements quantifier elimination over
+special-purpose dense linear orders using locales (analogous to
+"algebra"). The method is already installed for class
+{ordered_field,recpower,number_ring} which subsumes real, hyperreal,
+rat, etc.
+
* Former constant "List.op @" now named "List.append". Use ML
antiquotations @{const_name List.append} or @{term " ... @ ... "} to
circumvent possible incompatibilities when working on ML level.