--- a/src/HOL/OrderedGroup.thy Mon Mar 23 19:01:34 2009 +0100
+++ b/src/HOL/OrderedGroup.thy Mon Mar 23 13:26:52 2009 -0700
@@ -466,7 +466,7 @@
then show ?thesis by simp
qed
-lemma add_neg_nonpos:
+lemma add_neg_nonpos:
assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
proof -
have "a + b < 0 + 0"
@@ -494,6 +494,10 @@
then show ?thesis by simp
qed
+lemmas add_sign_intros =
+ add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
+ add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
+
lemma add_nonneg_eq_0_iff:
assumes x: "0 \<le> x" and y: "0 \<le> y"
shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"