
diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -604,7 +604,7 @@
 lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t"
   by (auto simp: analytic_on_def)
 
-lemma analytic_on_Union: "f analytic_on (\<Union> s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
+lemma analytic_on_Union: "f analytic_on (\<Union>s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
   by (auto simp: analytic_on_def)
 
 lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))"




