--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Apr 28 16:23:38 2015 +0100
@@ -240,7 +240,7 @@
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 isCont_ident isCont_const)+
+ isCont_Im continuous_ident continuous_const)+
lemma closed_complex_Reals: "closed (Reals :: complex set)"
proof -