# HG changeset patch
# User chaieb
# Date 1181318977 -7200
# Node ID 86e225406859464d155329a249c1a34ac70a85fe
# Parent  9302a50a5bc9f3917a09f1903ccdf8f9177ac5ac
Method "algebra" solves polynomial equations over (semi)rings

diff -r 9302a50a5bc9 -r 86e225406859 NEWS
--- a/NEWS	Fri Jun 08 03:24:27 2007 +0200
+++ b/NEWS	Fri Jun 08 18:09:37 2007 +0200
@@ -530,6 +530,16 @@
 
 *** HOL ***
 
+* Method "algebra" solves polynomial equations over (semi)rings using
+  Groebner bases. The (semi)ring structure is defined by locales and
+  the tool setup depends on that generic context. Installing the
+  method for a specific type involves instantiating the locale and
+  possibly adding declarations for computation on the coefficients.
+  The method is already instantiated for natural numbers and for the
+  axiomatic class of idoms with numerals.  See also the paper by
+  Chaieb and Wenzel at CALCULEMUS 2007 for the general principles
+  underlying this architecture of context-aware proof-tools.
+
 * 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.