NEWS
changeset 14399 dc677b35e54f
parent 14398 c5c47703f763
child 14401 477380c74c1d
--- a/NEWS	Thu Feb 19 15:57:34 2004 +0100
+++ b/NEWS	Thu Feb 19 16:44:21 2004 +0100
@@ -117,6 +117,8 @@
 
 * arith(_tac) is now able to generate counterexamples for reals as well.
 
+* HOL-Algebra: new locale "ring" for non-commutative rings.
+
 * SET-Protocol: formalization and verification of the SET protocol suite;
 
 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function