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/Hyperreal/MacLaurin.thy
changeset 16924 04246269386e
parent 16819 00d8f9300d13
child 19765 dfe940911617 
--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Jul 26 18:31:18 2005 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 27 11:28:18 2005 +0200
@@ -574,7 +574,7 @@
     apply (simp add: numeral_2_eq_2 divide_inverse)
     apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
                    simp add: est mult_nonneg_nonneg mult_ac divide_inverse
-                          power_abs [symmetric])
+                          power_abs [symmetric] abs_mult)
     done
 qed
isabelle