src/HOL/Real/RealDef.thy
changeset 15085 5693a977a767
parent 15077 89840837108e
child 15086 e6a2a98d5ef5
     1.1 --- a/src/HOL/Real/RealDef.thy	Thu Jul 29 16:14:06 2004 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jul 29 16:14:42 2004 +0200
     1.3 @@ -765,19 +765,19 @@
     1.4  lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" 
     1.5  by arith
     1.6  
     1.7 -lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)"
     1.8 +lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)"
     1.9  by auto
    1.10  
    1.11 -lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)"
    1.12 +lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)"
    1.13  by auto
    1.14  
    1.15 -lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)"
    1.16 +lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)"
    1.17  by auto
    1.18  
    1.19 -lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)"
    1.20 +lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> -x)"
    1.21  by auto
    1.22  
    1.23 -lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
    1.24 +lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)"
    1.25  by auto
    1.26  
    1.27  
    1.28 @@ -860,12 +860,6 @@
    1.29  ML
    1.30  {*
    1.31  val real_0_le_divide_iff = thm"real_0_le_divide_iff";
    1.32 -val real_add_minus_iff = thm"real_add_minus_iff";
    1.33 -val real_add_eq_0_iff = thm"real_add_eq_0_iff";
    1.34 -val real_add_less_0_iff = thm"real_add_less_0_iff";
    1.35 -val real_0_less_add_iff = thm"real_0_less_add_iff";
    1.36 -val real_add_le_0_iff = thm"real_add_le_0_iff";
    1.37 -val real_0_le_add_iff = thm"real_0_le_add_iff";
    1.38  val real_0_less_diff_iff = thm"real_0_less_diff_iff";
    1.39  val real_0_le_diff_iff = thm"real_0_le_diff_iff";
    1.40  val real_lbound_gt_zero = thm"real_lbound_gt_zero";