diff -r 5574d504cf36 -r 4ab9657b3257 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Sat Dec 29 15:43:53 2018 +0100
@@ -2433,7 +2433,7 @@
   using openin_subset by fastforce
 
 lemma compactin_euclideanreal_iff [simp]: "compactin euclideanreal S \<longleftrightarrow> compact S"
-  by (simp add: compact_eq_heine_borel compactin_def) meson
+  by (simp add: compact_eq_Heine_Borel compactin_def) meson
 
 lemma compactin_absolute [simp]:
    "compactin (subtopology X S) S \<longleftrightarrow> compactin X S"
@@ -2725,7 +2725,7 @@
 lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
   by (simp add: compactin_discrete_topology compact_space_def)
 
-lemma compact_space_imp_bolzano_weierstrass:
+lemma compact_space_imp_Bolzano_Weierstrass:
   assumes "compact_space X" "infinite S" "S \<subseteq> topspace X"
   shows "X derived_set_of S \<noteq> {}"
 proof
@@ -2738,19 +2738,19 @@
     by (metis \<open>infinite S\<close> compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq)
 qed
 
-lemma compactin_imp_bolzano_weierstrass:
+lemma compactin_imp_Bolzano_Weierstrass:
    "\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
-  using compact_space_imp_bolzano_weierstrass [of "subtopology X S"]
+  using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"]
   by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)
 
-lemma compact_closure_of_imp_bolzano_weierstrass:
+lemma compact_closure_of_imp_Bolzano_Weierstrass:
    "\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
-  using closure_of_mono closure_of_subset compactin_imp_bolzano_weierstrass by fastforce
+  using closure_of_mono closure_of_subset compactin_imp_Bolzano_Weierstrass by fastforce
 
 lemma discrete_compactin_eq_finite:
    "S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
   apply (rule iffI)
-  using compactin_imp_bolzano_weierstrass compactin_subset_topspace apply blast
+  using compactin_imp_Bolzano_Weierstrass compactin_subset_topspace apply blast
   by (simp add: finite_imp_compactin_eq)
 
 lemma discrete_compact_space_eq_finite: