clarified proposition
authorhaftmann
Fri Mar 07 13:53:03 2008 +0100 (2008-03-07)
changeset 262341f6e28a88785
parent 26233 3751b3dbb67c
child 26235 96b804999ca7
clarified proposition
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Mar 07 13:53:02 2008 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Mar 07 13:53:03 2008 +0100
     1.3 @@ -368,7 +368,7 @@
     1.4  lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
     1.5    by (drule mult_right_mono [of b zero], auto)
     1.6  
     1.7 -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)" 
     1.8 +lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
     1.9    by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
    1.10  
    1.11  end