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