src/HOL/RealVector.thy

   fix x y z :: 'a show "dist x y \<le> dist x z + dist y z"
     unfolding dist_norm
     using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
 qed
 
+subsection {* Extra type constraints *}
+
+text {* Only allow @{term dist} in class @{text metric_space}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
+
+text {* Only allow @{term norm} in class @{text real_normed_vector}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
+
 
 subsection {* Sign function *}
 
 lemma norm_sgn:
   "norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)"