summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | chaieb |

Fri, 08 Jun 2007 18:09:37 +0200 | |

changeset 23295 | 86e225406859 |

parent 23294 | 9302a50a5bc9 |

child 23296 | 25f28f9c28a3 |

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

--- 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.