src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy

     and open_halfspace_Im_lt: "open {z. Im(z) < b}"
     and open_halfspace_Im_gt: "open {z. Im(z) > b}"
     and closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
     and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
     and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
-  by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
-            isCont_Im continuous_ident continuous_const)+
+  by (intro open_Collect_less closed_Collect_le closed_Collect_eq continuous_on_Re
+            continuous_on_Im continuous_on_id continuous_on_const)+
 
 lemma closed_complex_Reals: "closed (\<real> :: complex set)"
 proof -
   have "(\<real> :: complex set) = {z. Im z = 0}"
     by (auto simp: complex_is_Real_iff)