--- a/src/HOL/Real_Vector_Spaces.thy Fri Apr 04 16:43:47 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Thu Apr 03 23:51:52 2014 +0100
@@ -1116,10 +1116,10 @@
by (simp add: sgn_div_norm divide_inverse)
lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
-unfolding real_sgn_eq by simp
+ by (rule sgn_pos)
lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
-unfolding real_sgn_eq by simp
+ by (rule sgn_neg)
lemma norm_conv_dist: "norm x = dist x 0"
unfolding dist_norm by simp