src/HOL/OrderedGroup.thy
changeset 30691 0047f57f6669
parent 30629 5cd9b19edef3
child 31016 e1309df633c6
     1.1 --- a/src/HOL/OrderedGroup.thy	Mon Mar 23 19:01:34 2009 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Mon Mar 23 13:26:52 2009 -0700
     1.3 @@ -466,7 +466,7 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma add_neg_nonpos: 
     1.8 +lemma add_neg_nonpos:
     1.9    assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
    1.10  proof -
    1.11    have "a + b < 0 + 0"
    1.12 @@ -494,6 +494,10 @@
    1.13    then show ?thesis by simp
    1.14  qed
    1.15  
    1.16 +lemmas add_sign_intros =
    1.17 +  add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
    1.18 +  add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
    1.19 +
    1.20  lemma add_nonneg_eq_0_iff:
    1.21    assumes x: "0 \<le> x" and y: "0 \<le> y"
    1.22    shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"