author | chaieb |

Fri Jun 08 18:09:37 2007 +0200 (2007-06-08) | |

changeset 23295 | 86e225406859 |

parent 23294 | 9302a50a5bc9 |

child 23296 | 25f28f9c28a3 |

Method "algebra" solves polynomial equations over (semi)rings

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.