src/HOL/Real_Vector_Spaces.thy
changeset 56479 91958d4b30f7
parent 56409 36489d77c484
child 56889 48a745e1bde7
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -1116,10 +1116,10 @@
     1.4  by (simp add: sgn_div_norm divide_inverse)
     1.5  
     1.6  lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
     1.7 -  by (rule sgn_pos)
     1.8 +unfolding real_sgn_eq by simp
     1.9  
    1.10  lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
    1.11 -  by (rule sgn_neg)
    1.12 +unfolding real_sgn_eq by simp
    1.13  
    1.14  lemma norm_conv_dist: "norm x = dist x 0"
    1.15    unfolding dist_norm by simp