# HG changeset patch
# User haftmann
# Date 1265710034 -3600
# Node ID 893062359becb9992a42b2b88d3b2d76b81cbb06
# Parent  be1e25a62ec8e4a79a3b9792d9a72ab636aba64b
dropped lemma duplicates

diff -r be1e25a62ec8 -r 893062359bec src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Tue Feb 09 08:28:12 2010 +0100
+++ b/src/HOL/Rational.thy	Tue Feb 09 11:07:14 2010 +0100
@@ -1083,14 +1083,6 @@
   finally show ?thesis using assms by simp
 qed
 
-lemma (in linordered_idom) sgn_greater [simp]:
-  "0 < sgn a \<longleftrightarrow> 0 < a"
-  unfolding sgn_if by auto
-
-lemma (in linordered_idom) sgn_less [simp]:
-  "sgn a < 0 \<longleftrightarrow> a < 0"
-  unfolding sgn_if by auto
-
 lemma rat_le_eq_code [code]:
   "Fract a b < Fract c d \<longleftrightarrow> (if b = 0
        then sgn c * sgn d > 0