equal
deleted
inserted
replaced
297 mult_left.diff ~> left_diff_distrib |
297 mult_left.diff ~> left_diff_distrib |
298 |
298 |
299 * Complex_Main: Several redundant theorems have been removed or |
299 * Complex_Main: Several redundant theorems have been removed or |
300 replaced by more general versions. INCOMPATIBILITY. |
300 replaced by more general versions. INCOMPATIBILITY. |
301 |
301 |
|
302 real_of_int_real_of_nat ~> real_of_int_of_nat_eq |
302 real_0_le_divide_iff ~> zero_le_divide_iff |
303 real_0_le_divide_iff ~> zero_le_divide_iff |
303 realpow_two_disj ~> power2_eq_iff |
304 realpow_two_disj ~> power2_eq_iff |
304 real_squared_diff_one_factored ~> square_diff_one_factored |
305 real_squared_diff_one_factored ~> square_diff_one_factored |
305 realpow_two_diff ~> square_diff_square_factored |
306 realpow_two_diff ~> square_diff_square_factored |
306 reals_complete2 ~> complete_real |
307 reals_complete2 ~> complete_real |