1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Sat Sep 30 14:32:36 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Sat Sep 30 17:10:55 2006 +0200
     1.3 @@ -100,6 +100,7 @@
     1.4  
     1.5  
     1.6  lemma Maclaurin_lemma3:
     1.7 +  fixes difg :: "nat => real => real" shows
     1.8       "[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t;
     1.9          \<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0;  n < m; 0 < t;
    1.10          t < h|]