diff -r 5cb5e7ecb284 -r ae0bbc8e45ad NEWS
--- a/NEWS	Wed Jan 04 21:28:28 2017 +0100
+++ b/NEWS	Wed Jan 04 21:28:29 2017 +0100
@@ -23,6 +23,11 @@
 use constants transp, antisymp, single_valuedp instead.
 INCOMPATIBILITY.
 
+* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
+euclidean_(semi)ring, euclidean_(semi)ring_cancel,
+unique_euclidean_(semi)ring; instantiation requires
+provision of a euclidean size.
+
 * Swapped orientation of congruence rules mod_add_left_eq,
 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
 mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,