--- a/src/HOL/Int.thy Sat Feb 14 10:24:15 2015 +0100
+++ b/src/HOL/Int.thy Sat Feb 14 10:24:15 2015 +0100
@@ -542,16 +542,6 @@
text {* Preliminaries *}
-lemma even_less_0_iff:
- "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
-proof -
- have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one)
- also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
- by (simp add: mult_less_0_iff zero_less_two
- order_less_not_sym [OF zero_less_two])
- finally show ?thesis .
-qed
-
lemma le_imp_0_less:
assumes le: "0 \<le> z"
shows "(0::int) < 1 + z"