NEWS
changeset 23295 86e225406859
parent 23251 471b576aad25
child 23300 b785068bd5dc
     1.1 --- a/NEWS	Fri Jun 08 03:24:27 2007 +0200
     1.2 +++ b/NEWS	Fri Jun 08 18:09:37 2007 +0200
     1.3 @@ -530,6 +530,16 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Method "algebra" solves polynomial equations over (semi)rings using
     1.8 +  Groebner bases. The (semi)ring structure is defined by locales and
     1.9 +  the tool setup depends on that generic context. Installing the
    1.10 +  method for a specific type involves instantiating the locale and
    1.11 +  possibly adding declarations for computation on the coefficients.
    1.12 +  The method is already instantiated for natural numbers and for the
    1.13 +  axiomatic class of idoms with numerals.  See also the paper by
    1.14 +  Chaieb and Wenzel at CALCULEMUS 2007 for the general principles
    1.15 +  underlying this architecture of context-aware proof-tools.
    1.16 +
    1.17  * constant "List.op @" now named "List.append".  Use ML antiquotations
    1.18  @{const_name List.append} or @{term " ... @ ... "} to circumvent
    1.19  possible incompatibilities when working on ML level.