equal
deleted
inserted
replaced
241 continuous_on_mul ~> continuous_on_scaleR |
241 continuous_on_mul ~> continuous_on_scaleR |
242 continuous_on_mul_real ~> continuous_on_mult |
242 continuous_on_mul_real ~> continuous_on_mult |
243 continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] |
243 continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] |
244 continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] |
244 continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] |
245 continuous_on_inverse ~> continuous_on_inv |
245 continuous_on_inverse ~> continuous_on_inv |
|
246 uniformly_continuous_on_neg ~> uniformly_continuous_on_minus |
|
247 uniformly_continuous_on_sub ~> uniformly_continuous_on_diff |
246 subset_interior ~> interior_mono |
248 subset_interior ~> interior_mono |
247 subset_closure ~> closure_mono |
249 subset_closure ~> closure_mono |
248 closure_univ ~> closure_UNIV |
250 closure_univ ~> closure_UNIV |
249 |
251 |
250 * Complex_Main: The locale interpretations for the bounded_linear and |
252 * Complex_Main: The locale interpretations for the bounded_linear and |