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.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.20
1.21 -lemma divide_minus_right [field_simps]:
1.22 +lemma divide_minus_right [simp]:
1.23    "a / - b = - (a / b)"
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.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:
```