# HG changeset patch
# User haftmann
# Date 1272023894 -7200
# Node ID c805033ad0327d27f94635f97309594193401ec1
# Parent  a35b83da74ce6911c26b41f33ee0de04c19ac32c
modernized abstract algebra theories

diff -r a35b83da74ce -r c805033ad032 NEWS
--- a/NEWS	Fri Apr 23 10:50:17 2010 +0200
+++ b/NEWS	Fri Apr 23 13:58:14 2010 +0200
@@ -112,6 +112,13 @@
 
 *** HOL ***
 
+* Abstract algebra:
+  * class division_by_zero includes division_ring;
+  * numerous lemmas have been ported from field to division_ring;
+  * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
+
+  INCOMPATIBILITY.
+
 * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
 provides abstract red-black tree type which is backed by RBT_Impl
 as implementation.  INCOMPATIBILTY.