# HG changeset patch
# User haftmann
# Date 1204894383 -3600
# Node ID 1f6e28a8878508562bbf78e26a9505445530ebf4
# Parent  3751b3dbb67c847da18886e46e94efe47c4453ee
clarified proposition

diff -r 3751b3dbb67c -r 1f6e28a88785 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Mar 07 13:53:02 2008 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Mar 07 13:53:03 2008 +0100
@@ -368,7 +368,7 @@
 lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   by (drule mult_right_mono [of b zero], auto)
 
-lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)" 
+lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
 
 end