equal
deleted
inserted
replaced
540 fderiv_def ~> has_derivative_at |
540 fderiv_def ~> has_derivative_at |
541 field_fderiv_def ~> field_has_derivative_at |
541 field_fderiv_def ~> field_has_derivative_at |
542 isDiff_der ~> differentiable_def |
542 isDiff_der ~> differentiable_def |
543 deriv_fderiv ~> has_field_derivative_def |
543 deriv_fderiv ~> has_field_derivative_def |
544 INCOMPATIBILITY. |
544 INCOMPATIBILITY. |
|
545 |
|
546 * Include more theorems in continuous_intros. Remove the continuous_on_intros, |
|
547 isCont_intros collections, these facts are now in continuous_intros. |
545 |
548 |
546 * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. |
549 * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. |
547 |
550 |
548 * Nitpick: |
551 * Nitpick: |
549 - Fixed soundness bug whereby mutually recursive datatypes could take |
552 - Fixed soundness bug whereby mutually recursive datatypes could take |