src/HOL/Rings.thy
changeset 54250 7d2544dd3988
parent 54230 b1d955791529
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Rings.thy	Mon Nov 04 20:10:06 2013 +0100
     1.2 +++ b/src/HOL/Rings.thy	Mon Nov 04 20:10:09 2013 +0100
     1.3 @@ -1145,10 +1145,6 @@
     1.4    thus ?thesis by (simp add: ac cpos mult_strict_mono) 
     1.5  qed
     1.6  
     1.7 -lemma less_minus_self_iff:
     1.8 -  "a < - a \<longleftrightarrow> a < 0"
     1.9 -  by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
    1.10 -
    1.11  lemma abs_less_iff:
    1.12    "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
    1.13    by (simp add: less_le abs_le_iff) (auto simp add: abs_if)