NEWS
changeset 64786 340db65fd2c1
parent 64785 ae0bbc8e45ad
child 64787 067cacdd1117
     1.1 --- a/NEWS	Wed Jan 04 21:28:29 2017 +0100
     1.2 +++ b/NEWS	Wed Jan 04 21:28:29 2017 +0100
     1.3 @@ -28,6 +28,15 @@
     1.4  unique_euclidean_(semi)ring; instantiation requires
     1.5  provision of a euclidean size.
     1.6  
     1.7 +* Reworking of theory Euclidean_Algorithm in session HOL-Number_Theory:
     1.8 +  - Euclidean induction is available as rule eucl_induct;
     1.9 +  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
    1.10 +    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
    1.11 +    easy instantiation of euclidean (semi)rings as GCD (semi)rings.
    1.12 +  - Coefficients obtained by extended euclidean algorithm are
    1.13 +    available as "bezout_coefficients".
    1.14 +INCOMPATIBILITY.
    1.15 +
    1.16  * Swapped orientation of congruence rules mod_add_left_eq,
    1.17  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.18  mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,