# HG changeset patch
# User chaieb
# Date 1182080390 -7200
# Node ID aed08cd6adae8e334dc5fb8dff10ffc9b57a1409
# Parent  c524900454f367774a6361edd03000af26dcca71
moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs

diff -r c524900454f3 -r aed08cd6adae src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Sun Jun 17 13:39:48 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Sun Jun 17 13:39:50 2007 +0200
@@ -227,15 +227,6 @@
 (* Caratheodory formulation of derivative at a point: standard proof        *)
 (* ------------------------------------------------------------------------ *)
 
-lemma nonzero_mult_divide_cancel_right:
-  "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
-proof -
-  assume b: "b \<noteq> 0"
-  have "a * b / b = a * (b / b)" by simp
-  also have "\<dots> = a" by (simp add: b)
-  finally show "a * b / b = a" .
-qed
-
 lemma CARAT_DERIV:
      "(DERIV f x :> l) =
       (\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isCont g x & g x = l)"
@@ -246,7 +237,7 @@
   proof (intro exI conjI)
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
     show "\<forall>z. f z - f x = ?g z * (z-x)"
-      by (simp add: nonzero_mult_divide_cancel_right)
+      by (simp add: nonzero_mult_divide_cancel_right')
     show "isCont ?g x" using der
       by (simp add: isCont_iff DERIV_iff diff_minus
                cong: LIM_equal [rule_format])
@@ -257,7 +248,7 @@
   then obtain g where
     "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
   thus "(DERIV f x :> l)"
-     by (auto simp add: isCont_iff DERIV_iff nonzero_mult_divide_cancel_right
+     by (auto simp add: isCont_iff DERIV_iff nonzero_mult_divide_cancel_right'
               cong: LIM_cong)
 qed