# HG changeset patch
# User haftmann
# Date 1233136932 -3600
# Node ID ece6a0e9f8af5880d7bc33ef546fa5faa0f975de
# Parent  f4c6e546b7fe6e586847f42477d1c6b399e23af9
added lemma abs_sng

diff -r f4c6e546b7fe -r ece6a0e9f8af src/HOL/Ring_and_Field.thy
--- 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