Method "algebra" solves polynomial equations over (semi)rings
authorchaieb
Fri Jun 08 18:09:37 2007 +0200 (2007-06-08)
changeset 2329586e225406859
parent 23294 9302a50a5bc9
child 23296 25f28f9c28a3
Method "algebra" solves polynomial equations over (semi)rings
NEWS
     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.