NEWS
changeset 64785 ae0bbc8e45ad
parent 64634 5bd30359e46e
child 64786 340db65fd2c1
     1.1 --- a/NEWS	Wed Jan 04 21:28:28 2017 +0100
     1.2 +++ b/NEWS	Wed Jan 04 21:28:29 2017 +0100
     1.3 @@ -23,6 +23,11 @@
     1.4  use constants transp, antisymp, single_valuedp instead.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
     1.8 +euclidean_(semi)ring, euclidean_(semi)ring_cancel,
     1.9 +unique_euclidean_(semi)ring; instantiation requires
    1.10 +provision of a euclidean size.
    1.11 +
    1.12  * Swapped orientation of congruence rules mod_add_left_eq,
    1.13  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.14  mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,