# HG changeset patch
# User huffman
# Date 1181023130 -7200
# Node ID e1526d5fa80dbe0359f396b9a8b357878a6205ad
# Parent  5f12b40a95bfb93a2f824122311b38799333ebab
remove simp attribute from lemma_STAR theorems

diff -r 5f12b40a95bf -r e1526d5fa80d src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Jun 05 00:54:03 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Jun 05 07:58:50 2007 +0200
@@ -420,7 +420,7 @@
 apply safe
 apply (simp (no_asm))
 apply (simp (no_asm))
-apply (case_tac "n", clarify, simp, simp)
+apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
diff -r 5f12b40a95bf -r e1526d5fa80d src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 00:54:03 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 07:58:50 2007 +0200
@@ -516,22 +516,22 @@
 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
 done
 
-lemma lemma_STAR_sin [simp]:
+lemma lemma_STAR_sin:
      "(if even n then 0  
        else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
 by (induct "n", auto)
 
-lemma lemma_STAR_cos [simp]:
+lemma lemma_STAR_cos:
      "0 < n -->  
       -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
 by (induct "n", auto)
 
-lemma lemma_STAR_cos1 [simp]:
+lemma lemma_STAR_cos1:
      "0 < n -->  
       (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
 by (induct "n", auto)
 
-lemma lemma_STAR_cos2 [simp]:
+lemma lemma_STAR_cos2:
   "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n 
                          else 0) = 0"
 apply (induct "n")
@@ -1001,7 +1001,7 @@
 
 lemma sin_zero [simp]: "sin 0 = 0"
 by (auto intro!: sums_unique [symmetric] LIMSEQ_const 
-         simp add: sin_def sums_def simp del: power_0_left)
+         simp add: sin_def sums_def lemma_STAR_sin)
 
 lemma lemma_series_zero2:
  "(\<forall>m. n \<le> m --> f m = 0) --> f sums setsum f {0..<n}"