25 |
25 |
26 * Algebraic type class hierarchy of euclidean (semi)rings in HOL: |
26 * Algebraic type class hierarchy of euclidean (semi)rings in HOL: |
27 euclidean_(semi)ring, euclidean_(semi)ring_cancel, |
27 euclidean_(semi)ring, euclidean_(semi)ring_cancel, |
28 unique_euclidean_(semi)ring; instantiation requires |
28 unique_euclidean_(semi)ring; instantiation requires |
29 provision of a euclidean size. |
29 provision of a euclidean size. |
|
30 |
|
31 * Reworking of theory Euclidean_Algorithm in session HOL-Number_Theory: |
|
32 - Euclidean induction is available as rule eucl_induct; |
|
33 - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm, |
|
34 Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow |
|
35 easy instantiation of euclidean (semi)rings as GCD (semi)rings. |
|
36 - Coefficients obtained by extended euclidean algorithm are |
|
37 available as "bezout_coefficients". |
|
38 INCOMPATIBILITY. |
30 |
39 |
31 * Swapped orientation of congruence rules mod_add_left_eq, |
40 * Swapped orientation of congruence rules mod_add_left_eq, |
32 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, |
41 mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, |
33 mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, |
42 mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, |
34 mod_diff_eq. INCOMPATIBILITY. |
43 mod_diff_eq. INCOMPATIBILITY. |