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 16775 c1b87ef4a1c3
parent 15944 9b00875e21f7
child 16819 00d8f9300d13 
--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Jul 12 12:49:46 2005 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Jul 12 17:56:03 2005 +0200
@@ -600,7 +600,7 @@
     apply (drule lemma_odd_mod_4_div_2)
     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_pos_le mult_ac divide_inverse
+                   simp add: est mult_nonneg_nonneg mult_ac divide_inverse
                           power_abs [symmetric])
     done
 qed
isabelle