--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat Dec 29 15:43:53 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat Dec 29 16:58:53 2018 +0100
@@ -5688,7 +5688,7 @@
using uwd by (simp add: dist_commute dist_norm)
have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
\<le> (real k * 4 + real k * real k * 4) * (cmod (u - w) * cmod (u - w)) / (d * (d * (d/2) ^ k))"
- using complex_taylor [OF _ ff1 ff2 _ ub, of w, simplified]
+ using complex_Taylor [OF _ ff1 ff2 _ ub, of w, simplified]
by (simp add: ff_def \<open>0 < d\<close>)
then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
\<le> (cmod (u - w) * real k) * (1 + real k) * cmod (u - w) / (d/2) ^ (k+2)"
--- a/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy Sat Dec 29 15:43:53 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy Sat Dec 29 16:58:53 2018 +0100
@@ -75,7 +75,7 @@
where "compact_with \<equiv> \<lambda>open S. (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
lemma compact_compact_with: "compact s = compact_with open s"
- unfolding compact_with_def compact_eq_heine_borel[abs_def] ..
+ unfolding compact_with_def compact_eq_Heine_Borel[abs_def] ..
definition compact_on_with :: "'a set \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
where "compact_on_with A \<equiv> \<lambda>open S. (\<forall>C\<subseteq>Pow A. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow>