# HG changeset patch
# User wenzelm
# Date 1247169850 -7200
# Node ID a89f758dba5bdca66d6f50549bb256b60ab0023e
# Parent  8c1b845ed1057d989b117b87b7dab15293fefb43# Parent  02f02097e1e4d3ff83b2dca938dfe344199314fe
merged

diff -r 8c1b845ed105 -r a89f758dba5b src/HOL/ex/Formal_Power_Series_Examples.thy
--- a/src/HOL/ex/Formal_Power_Series_Examples.thy	Thu Jul 09 22:01:41 2009 +0200
+++ b/src/HOL/ex/Formal_Power_Series_Examples.thy	Thu Jul 09 22:04:10 2009 +0200
@@ -184,9 +184,10 @@
 qed
 
 lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c "
-  unfolding minus_mult_right Eii_sin_cos by simp
+  unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
 
-lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)  "by (simp add: fps_eq_iff fps_const_def)
+lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
+  by (simp add: fps_eq_iff fps_const_def)
 
 lemma fps_number_of_fps_const: "number_of i = fps_const (number_of i :: 'a:: {comm_ring_1, number_ring})"
   apply (subst (2) number_of_eq)
@@ -201,7 +202,8 @@
     by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   show ?thesis
   unfolding Eii_sin_cos minus_mult_commute
-  by (simp add: fps_number_of_fps_const fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
+  by (simp add: fps_sin_even fps_cos_odd fps_number_of_fps_const
+    fps_divide_def fps_const_inverse th complex_number_of_def[symmetric])
 qed
 
 lemma fps_sin_Eii:
@@ -211,7 +213,7 @@
     by (simp add: fps_eq_iff fps_number_of_fps_const complex_number_of_def[symmetric])
   show ?thesis
   unfolding Eii_sin_cos minus_mult_commute
-  by (simp add: fps_divide_def fps_const_inverse th)
+  by (simp add: fps_sin_even fps_cos_odd fps_divide_def fps_const_inverse th)
 qed
 
 lemma fps_const_mult_2: "fps_const (2::'a::number_ring) * a = a +a"