equal
deleted
inserted
replaced
90 - Auto Sledgehammer now minimizes and preplays the results. |
90 - Auto Sledgehammer now minimizes and preplays the results. |
91 |
91 |
92 * Nitpick: |
92 * Nitpick: |
93 - Removed "check_potential" and "check_genuine" options. |
93 - Removed "check_potential" and "check_genuine" options. |
94 |
94 |
|
95 * Tightened specification of class semiring_no_zero_divisors. Slight |
|
96 INCOMPATIBILITY. |
|
97 |
95 * Former constants Fields.divide (_ / _) and Divides.div (_ div _) |
98 * Former constants Fields.divide (_ / _) and Divides.div (_ div _) |
96 are logically unified to Rings.divide in syntactic type class |
99 are logically unified to Rings.divide in syntactic type class |
97 Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) |
100 Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) |
98 for field division is added later as abbreviation in class Fields.inverse. |
101 for field division is added later as abbreviation in class Fields.inverse. |
99 INCOMPATIBILITY, instantiatios must refer to Rings.divide rather |
102 INCOMPATIBILITY, instantiations must refer to Rings.divide rather |
100 than the former separate constants, hence infix syntax (_ / _) is usually |
103 than the former separate constants, hence infix syntax (_ / _) is usually |
101 not available during instantiation. |
104 not available during instantiation. |
102 |
105 |
103 * Library/Multiset: |
106 * Library/Multiset: |
104 - Renamed multiset inclusion operators: |
107 - Renamed multiset inclusion operators: |