src/HOL/Real_Vector_Spaces.thy
changeset 62102 877463945ce9
parent 62101 26c0a70f78a3
child 62131 1baed43f453e
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 17:41:04 2016 +0100
     1.3 @@ -9,7 +9,6 @@
     1.4  imports Real Topological_Spaces
     1.5  begin
     1.6  
     1.7 -
     1.8  lemma (in ordered_ab_group_add) diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
     1.9    by (simp add: le_diff_eq)
    1.10  
    1.11 @@ -1185,6 +1184,8 @@
    1.12  
    1.13  end
    1.14  
    1.15 +declare uniformity_Abort[where 'a=real, code]
    1.16 +
    1.17  lemma dist_of_real [simp]:
    1.18    fixes a :: "'a::real_normed_div_algebra"
    1.19    shows "dist (of_real x :: 'a) (of_real y) = dist x y"