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 \ t) \ f analytic_on s \ f analytic_on t" by (auto simp: analytic_on_def) -lemma analytic_on_Union: "f analytic_on (\ s) \ (\t \ s. f analytic_on t)" +lemma analytic_on_Union: "f analytic_on (\s) \ (\t \ s. f analytic_on t)" by (auto simp: analytic_on_def) lemma analytic_on_UN: "f analytic_on (\i\I. s i) \ (\i\I. f analytic_on (s i))"