--- a/src/HOL/Limits.thy Sun Mar 17 21:26:42 2019 +0100
+++ b/src/HOL/Limits.thy Mon Mar 18 15:35:34 2019 +0000
@@ -532,6 +532,9 @@
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
unfolding continuous_on_def by (auto intro: tendsto_dist)
+lemma continuous_at_dist: "isCont (dist a) b"
+ using continuous_on_dist [OF continuous_on_const continuous_on_id] continuous_on_eq_continuous_within by blast
+
lemma tendsto_norm [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> norm a) F"
unfolding norm_conv_dist by (intro tendsto_intros)