changeset 20792 | add17d26151b |
parent 20217 | 25b068a99d2b |
child 21782 | bf055d30d3ad |
--- a/src/HOL/Hyperreal/MacLaurin.thy Sat Sep 30 14:32:36 2006 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Sat Sep 30 17:10:55 2006 +0200 @@ -100,6 +100,7 @@ lemma Maclaurin_lemma3: + fixes difg :: "nat => real => real" shows "[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t; \<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0; n < m; 0 < t; t < h|]