equal
deleted
inserted
replaced
134 int_0_neq_1 ~> zero_neq_one |
134 int_0_neq_1 ~> zero_neq_one |
135 zless_le ~> less_le |
135 zless_le ~> less_le |
136 zpower_zadd_distrib ~> power_add |
136 zpower_zadd_distrib ~> power_add |
137 zero_less_zpower_abs_iff ~> zero_less_power_abs_iff |
137 zero_less_zpower_abs_iff ~> zero_less_power_abs_iff |
138 zero_le_zpower_abs ~> zero_le_power_abs |
138 zero_le_zpower_abs ~> zero_le_power_abs |
|
139 |
|
140 * Theory Deriv: Renamed |
|
141 |
|
142 DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing |
139 |
143 |
140 * New "case_product" attribute to generate a case rule doing multiple |
144 * New "case_product" attribute to generate a case rule doing multiple |
141 case distinctions at the same time. E.g. |
145 case distinctions at the same time. E.g. |
142 |
146 |
143 list.exhaust [case_product nat.exhaust] |
147 list.exhaust [case_product nat.exhaust] |