src/HOL/Fields.thy
changeset 56479 91958d4b30f7
parent 56445 82ce19612fe8
child 56480 093ea91498e6
     1.1 --- a/src/HOL/Fields.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Fields.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -152,11 +152,11 @@
     1.4  lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
     1.5    by (simp add: divide_inverse nonzero_inverse_minus_eq)
     1.6  
     1.7 -lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)"
     1.8 +lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
     1.9    by (simp add: divide_inverse)
    1.10  
    1.11  lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
    1.12 -  using add_divide_distrib [of a "- b" c] by (simp add: divide_inverse)
    1.13 +  using add_divide_distrib [of a "- b" c] by simp
    1.14  
    1.15  lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
    1.16  proof -
    1.17 @@ -416,11 +416,11 @@
    1.18    "- (a / b) = a / - b"
    1.19    by (simp add: divide_inverse)
    1.20  
    1.21 -lemma divide_minus_right [field_simps]:
    1.22 +lemma divide_minus_right [simp]:
    1.23    "a / - b = - (a / b)"
    1.24    by (simp add: divide_inverse)
    1.25  
    1.26 -lemma minus_divide_divide [simp]:
    1.27 +lemma minus_divide_divide:
    1.28    "(- a) / (- b) = a / b"
    1.29  apply (cases "b=0", simp) 
    1.30  apply (simp add: nonzero_minus_divide_divide) 
    1.31 @@ -1053,13 +1053,13 @@
    1.32  lemma divide_right_mono_neg: "a <= b 
    1.33      ==> c <= 0 ==> b / c <= a / c"
    1.34  apply (drule divide_right_mono [of _ _ "- c"])
    1.35 -apply (auto simp: divide_minus_right)
    1.36 +apply auto
    1.37  done
    1.38  
    1.39  lemma divide_left_mono_neg: "a <= b 
    1.40      ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
    1.41    apply (drule divide_left_mono [of _ _ "- c"])
    1.42 -  apply (auto simp add: divide_minus_left mult_commute)
    1.43 +  apply (auto simp add: mult_commute)
    1.44  done
    1.45  
    1.46  lemma inverse_le_iff: