equal
deleted
inserted
replaced
119 Suc_not_Zero Zero_not_Suc ~> nat.distinct |
119 Suc_not_Zero Zero_not_Suc ~> nat.distinct |
120 |
120 |
121 * Library/Nat_Infinity: added addition, numeral syntax and more |
121 * Library/Nat_Infinity: added addition, numeral syntax and more |
122 instantiations for algebraic structures. Removed some duplicate |
122 instantiations for algebraic structures. Removed some duplicate |
123 theorems. Changes in simp rules. INCOMPATIBILITY. |
123 theorems. Changes in simp rules. INCOMPATIBILITY. |
|
124 |
|
125 |
|
126 *** HOL-Algebra *** |
|
127 |
|
128 * Units_l_inv and Units_r_inv are now simprules by default. |
|
129 INCOMPATIBILITY. Simplifier proof that require deletion of l_inv |
|
130 and/or r_inv will now also require deletion of these lemmas. |
|
131 |
|
132 * Renamed the following theorems. INCOMPATIBILITY. |
|
133 UpperD ~> Upper_memD |
|
134 LowerD ~> Lower_memD |
|
135 least_carrier ~> least_closed |
|
136 greatest_carrier ~> greatest_closed |
|
137 greatest_Lower_above ~> greatest_Lower_below |
|
138 |
|
139 * New theory of factorial domains. |
124 |
140 |
125 |
141 |
126 *** HOL-NSA *** |
142 *** HOL-NSA *** |
127 |
143 |
128 * Created new image HOL-NSA, containing theories of nonstandard |
144 * Created new image HOL-NSA, containing theories of nonstandard |