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: 