src/HOL/Ring_and_Field.thy
 changeset 25078 a1ddc5206cb1 parent 25062 af5ef0d4d655 child 25152 bfde2f8c0f63
```     1.1 --- a/src/HOL/Ring_and_Field.thy	Thu Oct 18 09:20:57 2007 +0200
1.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Oct 18 09:20:58 2007 +0200
1.3 @@ -1977,8 +1977,8 @@
1.4        apply (insert prems)
1.6  	ring_simps
1.7 -	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
1.8 -	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
1.9 +	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
1.10 +	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
1.11  	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
1.12  	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
1.13        done
1.14 @@ -2127,25 +2127,4 @@
1.15    then show ?thesis by simp
1.16  qed
1.17
1.18 -
1.19 -subsection {* Theorems for proof tools *}
1.20 -
1.22 -  fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
1.23 -  shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
1.24 -    and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
1.25 -    and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
1.26 -    and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"