diff -r 4c53227f4b73 -r 3d894e1cfc75 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Sep 12 14:51:45 2019 +0100
@@ -1100,34 +1100,6 @@
     by (simp add: fun_Compl_def uniformly_continuous_on_minus)
 
 
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological properties of linear functions\<close>
-
-lemma linear_lim_0:
-  assumes "bounded_linear f"
-  shows "(f \<longlongrightarrow> 0) (at (0))"
-proof -
-  interpret f: bounded_linear f by fact
-  have "(f \<longlongrightarrow> f 0) (at 0)"
-    using tendsto_ident_at by (rule f.tendsto)
-  then show ?thesis unfolding f.zero .
-qed
-
-lemma linear_continuous_at:
-  assumes "bounded_linear f"
-  shows "continuous (at a) f"
-  unfolding continuous_at using assms
-  apply (rule bounded_linear.tendsto)
-  apply (rule tendsto_ident_at)
-  done
-
-lemma linear_continuous_within:
-  "bounded_linear f \<Longrightarrow> continuous (at x within s) f"
-  using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
-
-lemma linear_continuous_on:
-  "bounded_linear f \<Longrightarrow> continuous_on s f"
-  using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>
 
 lemma open_scaling[intro]: