# 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 \ 0 < a" - unfolding sgn_if by auto - -lemma (in linordered_idom) sgn_less [simp]: - "sgn a < 0 \ a < 0" - unfolding sgn_if by auto - lemma rat_le_eq_code [code]: "Fract a b < Fract c d \ (if b = 0 then sgn c * sgn d > 0