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

author | ballarin |

Wed, 19 Jul 2006 23:22:22 +0200 | |

changeset 20169 | 52173f7687fd |

parent 20168 | ed7bced29e1b |

child 20170 | 6ff853f82d73 |

Change to algebra method.

--- a/NEWS Wed Jul 19 19:25:58 2006 +0200 +++ b/NEWS Wed Jul 19 23:22:22 2006 +0200 @@ -497,6 +497,11 @@ * Support for hex (0x20) and binary (0b1001) numerals. +*** HOL-Algebra *** + +* Method algebra is now set up via an attribute. For examples see CRing.thy. + INCOMPATIBILITY: the method is now weaker on combinations of algebraic structures. + *** HOL-Complex *** * Theory Real: new method ferrack implements quantifier elimination