src/HOL/Real_Vector_Spaces.thy

 section \<open>Vector Spaces and Algebras over the Reals\<close>
 
 theory Real_Vector_Spaces
 imports Real Topological_Spaces
 begin
-
 
 lemma (in ordered_ab_group_add) diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   by (simp add: le_diff_eq)
 
 subsection \<open>Locale for additive functions\<close>

 apply (rule abs_mult)
 apply (rule abs_mult)
 done
 
 end
+
+declare uniformity_Abort[where 'a=real, code]
 
 lemma dist_of_real [simp]:
   fixes a :: "'a::real_normed_div_algebra"
   shows "dist (of_real x :: 'a) (of_real y) = dist x y"
 by (metis dist_norm norm_of_real of_real_diff real_norm_def)