equal
deleted
inserted
replaced
86 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
86 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
87 token category instead. |
87 token category instead. |
88 |
88 |
89 |
89 |
90 *** HOL *** |
90 *** HOL *** |
|
91 |
|
92 * Given up separate type class no_zero_divisors in favour of fully algebraic |
|
93 semiring_no_zero_divisors. INCOMPATIBILITY. |
|
94 |
|
95 * Class linordered_semidom really requires no zero divisors. |
|
96 INCOMPATIBILITY. |
|
97 |
|
98 * Classes division_ring, field and linordered_field always demand |
|
99 `inverse 0 = 0`. Given up separate classes division_ring_inverse_zero, |
|
100 field_inverse_zero and linordered_field_inverse_zero. |
|
101 INCOMPATIBILITY. |
91 |
102 |
92 * Type classes cancel_ab_semigroup_add / cancel_monoid_add specify |
103 * Type classes cancel_ab_semigroup_add / cancel_monoid_add specify |
93 explicit additive inverse operation. INCOMPATIBILITY. |
104 explicit additive inverse operation. INCOMPATIBILITY. |
94 |
105 |
95 * New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for |
106 * New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for |