--- a/src/HOL/Real_Vector_Spaces.thy Fri Jan 08 17:40:59 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Jan 08 17:41:04 2016 +0100
@@ -9,7 +9,6 @@
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)
@@ -1185,6 +1184,8 @@
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"