# HG changeset patch
# User nipkow
# Date 1546099133 -3600
# Node ID fc0da2166cda0631609a2953a20b5b646f7e780f
# Parent  4ab9657b325718052f054a77c943e9cbf5192a0b
more capitalization

diff -r 4ab9657b3257 -r fc0da2166cda src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- 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)"
diff -r 4ab9657b3257 -r fc0da2166cda src/HOL/Types_To_Sets/Examples/T2_Spaces.thy
--- 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>