changeset 23242 | e1526d5fa80d |
parent 23177 | 3004310c95b1 |
child 24180 | 9f818139951b |
--- 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)