# HG changeset patch
# User huffman
# Date 1237840012 25200
# Node ID 0047f57f6669ff1119e8453b04064fcfbb547150
# Parent  55ef8e0459315463e19f9bc3c436b661d2dd2761
lemmas add_sign_intros

diff -r 55ef8e045931 -r 0047f57f6669 src/HOL/OrderedGroup.thy
--- 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"