--- a/NEWS Sat Feb 14 10:24:15 2015 +0100
+++ b/NEWS Sat Feb 14 10:24:15 2015 +0100
@@ -68,6 +68,9 @@
*** HOL ***
+* Fact consolidation: even_less_0_iff is subsumed by
+double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
+
* Discontinued old-fashioned "codegen" tool. Code generation can always
be externally triggered using an appropriate ROOT file plus a corresponding
theory. Parametrization is possible using environment variables, or
--- 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"