Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Gauge_Integration.thy
changeset 49962 a8cc904a6820
parent 46501 fe51817749d1
child 51480 3793c3a11378 
--- a/src/HOL/ex/Gauge_Integration.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -521,9 +521,9 @@
                     = (f z - f x) / (z - x) - f' x")
  apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
 apply (subst mult_commute)
-apply (simp add: left_distrib diff_minus)
+apply (simp add: distrib_right diff_minus)
 apply (simp add: mult_assoc divide_inverse)
-apply (simp add: left_distrib)
+apply (simp add: distrib_right)
 done
 
 lemma lemma_straddle:
isabelle