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/Library/Formal_Power_Series.thy
changeset 56410 a14831ac3023
parent 55159 608c157d743d
child 56479 91958d4b30f7 
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -3635,7 +3635,7 @@
   done
 
 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c"
-  by (auto simp add: fps_eq_iff fps_sin_def)
+  by (auto simp add: divide_minus_left fps_eq_iff fps_sin_def)
 
 lemma fps_cos_odd: "fps_cos (- c) = fps_cos c"
   by (auto simp add: fps_eq_iff fps_cos_def)
isabelle