author haftmann Thu, 18 Oct 2007 09:20:58 +0200 changeset 25078 a1ddc5206cb1 parent 25077 c2ec5e589d78 child 25079 db5fdc34f3af
moved lemmas to OrderedGroup.thy
```--- a/src/HOL/Ring_and_Field.thy	Thu Oct 18 09:20:57 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Oct 18 09:20:58 2007 +0200
@@ -1977,8 +1977,8 @@
apply (insert prems)
ring_simps
-	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
-	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
+	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
+	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
apply(drule (1) mult_nonneg_nonpos[of a b], simp)
apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
done
@@ -2127,25 +2127,4 @@
then show ?thesis by simp
qed

-
-subsection {* Theorems for proof tools *}
-
-  fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
-  shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
-    and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
-    and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
-    and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"