dropped redundancy
authorhaftmann
Sat Feb 14 10:24:15 2015 +0100 (2015-02-14)
changeset 5953603bde055a1a0
parent 59535 9e7467829db5
child 59537 7f2b60cb5190
dropped redundancy
NEWS
src/HOL/Int.thy
     1.1 --- a/NEWS	Sat Feb 14 10:24:15 2015 +0100
     1.2 +++ b/NEWS	Sat Feb 14 10:24:15 2015 +0100
     1.3 @@ -68,6 +68,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Fact consolidation: even_less_0_iff is subsumed by
     1.8 +double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
     1.9 +
    1.10  * Discontinued old-fashioned "codegen" tool.  Code generation can always
    1.11  be externally triggered using an appropriate ROOT file plus a corresponding
    1.12  theory.  Parametrization is possible using environment variables, or
     2.1 --- a/src/HOL/Int.thy	Sat Feb 14 10:24:15 2015 +0100
     2.2 +++ b/src/HOL/Int.thy	Sat Feb 14 10:24:15 2015 +0100
     2.3 @@ -542,16 +542,6 @@
     2.4  
     2.5  text {* Preliminaries *}
     2.6  
     2.7 -lemma even_less_0_iff:
     2.8 -  "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
     2.9 -proof -
    2.10 -  have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one)
    2.11 -  also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
    2.12 -    by (simp add: mult_less_0_iff zero_less_two 
    2.13 -                  order_less_not_sym [OF zero_less_two])
    2.14 -  finally show ?thesis .
    2.15 -qed
    2.16 -
    2.17  lemma le_imp_0_less: 
    2.18    assumes le: "0 \<le> z"
    2.19    shows "(0::int) < 1 + z"