# HG changeset patch
# User haftmann
# Date 1423905855 -3600
# Node ID 03bde055a1a04535c40016aecec09875f6ccacf0
# Parent  9e7467829db56e633198e9bbee31c5a56c243274
dropped redundancy

diff -r 9e7467829db5 -r 03bde055a1a0 NEWS
--- 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
diff -r 9e7467829db5 -r 03bde055a1a0 src/HOL/Int.thy
--- 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"