# HG changeset patch
# User nipkow
# Date 1396810905 -7200
# Node ID 70a13de8a154cb7a705705e653973cb077c142dc
# Parent  f944ae8c80a3735f1f3b1fa1abbea324c08750c8# Parent  82ce19612fe8d41eeece750d6880135a7c291142
merged

diff -r f944ae8c80a3 -r 70a13de8a154 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sun Apr 06 19:35:35 2014 +0200
+++ b/src/HOL/Fields.thy	Sun Apr 06 21:01:45 2014 +0200
@@ -188,6 +188,22 @@
 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
   by (drule sym) (simp add: divide_inverse mult_assoc)
 
+lemma add_divide_eq_iff [field_simps]:
+  "z \<noteq> 0 \<Longrightarrow> x + y / z = (x * z + y) / z"
+  by (simp add: add_divide_distrib nonzero_eq_divide_eq)
+
+lemma divide_add_eq_iff [field_simps]:
+  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + y * z) / z"
+  by (simp add: add_divide_distrib nonzero_eq_divide_eq)
+
+lemma diff_divide_eq_iff [field_simps]:
+  "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 divide_diff_eq_iff [field_simps]:
+  "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z"
+  by (simp add: field_simps)
+
 end
 
 class division_ring_inverse_zero = division_ring +
@@ -323,22 +339,6 @@
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
 using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
 
-lemma add_divide_eq_iff [field_simps]:
-  "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
-  by (simp add: add_divide_distrib)
-
-lemma divide_add_eq_iff [field_simps]:
-  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
-  by (simp add: add_divide_distrib)
-
-lemma diff_divide_eq_iff [field_simps]:
-  "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
-  by (simp add: diff_divide_distrib)
-
-lemma divide_diff_eq_iff [field_simps]:
-  "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
-  by (simp add: diff_divide_distrib)
-
 lemma diff_frac_eq:
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
   by (simp add: field_simps)
diff -r f944ae8c80a3 -r 70a13de8a154 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Apr 06 19:35:35 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Apr 06 21:01:45 2014 +0200
@@ -127,7 +127,7 @@
   "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
 proof -
   have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
-    by (metis divide_diff_eq_iff eq_iff_diff_eq_0)
+    by (metis divide_diff_eq_iff eq_iff_diff_eq_0 mult_commute)
   show ?thesis
     apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
     apply (simp add: LIM_zero_iff [where l = D, symmetric])