1.1 --- a/src/HOL/Rational.thy	Tue Feb 09 08:28:12 2010 +0100
     1.2 +++ b/src/HOL/Rational.thy	Tue Feb 09 11:07:14 2010 +0100
     1.3 @@ -1083,14 +1083,6 @@
     1.4    finally show ?thesis using assms by simp
     1.5  qed
     1.6  
     1.7 -lemma (in linordered_idom) sgn_greater [simp]:
     1.8 -  "0 < sgn a \<longleftrightarrow> 0 < a"
     1.9 -  unfolding sgn_if by auto
    1.10 -
    1.11 -lemma (in linordered_idom) sgn_less [simp]:
    1.12 -  "sgn a < 0 \<longleftrightarrow> a < 0"
    1.13 -  unfolding sgn_if by auto
    1.14 -
    1.15  lemma rat_le_eq_code [code]:
    1.16    "Fract a b < Fract c d \<longleftrightarrow> (if b = 0
    1.17         then sgn c * sgn d > 0