20 INCOMPATIBILITY. |
20 INCOMPATIBILITY. |
21 |
21 |
22 * Dropped abbreviation transP, antisymP, single_valuedP; |
22 * Dropped abbreviation transP, antisymP, single_valuedP; |
23 use constants transp, antisymp, single_valuedp instead. |
23 use constants transp, antisymp, single_valuedp instead. |
24 INCOMPATIBILITY. |
24 INCOMPATIBILITY. |
|
25 |
|
26 * Algebraic type class hierarchy of euclidean (semi)rings in HOL: |
|
27 euclidean_(semi)ring, euclidean_(semi)ring_cancel, |
|
28 unique_euclidean_(semi)ring; instantiation requires |
|
29 provision of a euclidean size. |
25 |
30 |
26 * Swapped orientation of congruence rules mod_add_left_eq, |
31 * Swapped orientation of congruence rules mod_add_left_eq, |
27 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, |
32 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, |
28 mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, |
33 mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, |
29 mod_diff_eq. INCOMPATIBILITY. |
34 mod_diff_eq. INCOMPATIBILITY. |