src/HOL/Fields.thy

   also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult.assoc) 
   finally show ?thesis .
 qed
 
 lemma nonzero_neg_divide_eq_eq [field_simps]: "b \<noteq> 0 \<Longrightarrow> - (a / b) = c \<longleftrightarrow> - a = c * b"
-  using nonzero_divide_eq_eq[of b "-a" c] by (simp add: divide_minus_left)
+  using nonzero_divide_eq_eq[of b "-a" c] by simp
 
 lemma nonzero_neg_divide_eq_eq2 [field_simps]: "b \<noteq> 0 \<Longrightarrow> c = - (a / b) \<longleftrightarrow> c * b = - a"
   using nonzero_neg_divide_eq_eq[of b a c] by auto
 
 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"

   "z \<noteq> 0 \<Longrightarrow> x - y / z = (x * z - y) / z"
   by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq)
 
 lemma minus_divide_add_eq_iff [field_simps]:
   "z \<noteq> 0 \<Longrightarrow> - (x / z) + y = (- x + y * z) / z"
-  by (simp add: add_divide_distrib diff_divide_eq_iff divide_minus_left)
+  by (simp add: add_divide_distrib diff_divide_eq_iff)
 
 lemma divide_diff_eq_iff [field_simps]:
   "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z"
   by (simp add: field_simps)
 
 lemma minus_divide_diff_eq_iff [field_simps]:
   "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
-  by (simp add: divide_diff_eq_iff[symmetric] divide_minus_left)
+  by (simp add: divide_diff_eq_iff[symmetric])
 
 end
 
 class division_ring_inverse_zero = division_ring +
   assumes inverse_zero [simp]: "inverse 0 = 0"