diff -r ae0bbc8e45ad -r 340db65fd2c1 NEWS
--- a/NEWS	Wed Jan 04 21:28:29 2017 +0100
+++ b/NEWS	Wed Jan 04 21:28:29 2017 +0100
@@ -28,6 +28,15 @@
 unique_euclidean_(semi)ring; instantiation requires
 provision of a euclidean size.
 
+* Reworking of theory Euclidean_Algorithm in session HOL-Number_Theory:
+  - Euclidean induction is available as rule eucl_induct;
+  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
+    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
+    easy instantiation of euclidean (semi)rings as GCD (semi)rings.
+  - Coefficients obtained by extended euclidean algorithm are
+    available as "bezout_coefficients".
+INCOMPATIBILITY.
+
 * 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,