--- a/src/HOL/Fields.thy Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Fields.thy Fri Apr 04 17:58:25 2014 +0100
@@ -152,7 +152,7 @@
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
by (simp add: divide_inverse nonzero_inverse_minus_eq)
-lemma divide_minus_left: "(-a) / b = - (a / b)"
+lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)"
by (simp add: divide_inverse)
lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
@@ -408,7 +408,7 @@
"- (a / b) = a / - b"
by (simp add: divide_inverse)
-lemma divide_minus_right:
+lemma divide_minus_right [field_simps]:
"a / - b = - (a / b)"
by (simp add: divide_inverse)