added lemma abs_sng

--- a/src/HOL/Ring_and_Field.thy	Wed Jan 28 11:02:12 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Wed Jan 28 11:02:12 2009 +0100
@@ -1091,6 +1091,9 @@
   "sgn (a * b) = sgn a * sgn b"
   by (auto simp add: sgn_if zero_less_mult_iff)
 
+lemma abs_sgn: "abs k = k * sgn k"
+  unfolding sgn_if abs_if by auto
+
 end
 
 class ordered_field = field + ordered_idom