src/HOL/Hyperreal/MacLaurin.thy
changeset 15131 c69542757a4d
parent 15081 32402f5624d1
child 15140 322485b816ac
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Aug 16 14:21:54 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon Aug 16 14:22:27 2004 +0200
     1.3 @@ -5,7 +5,9 @@
     1.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.5  *)
     1.6  
     1.7 -theory MacLaurin = Log:
     1.8 +theory MacLaurin
     1.9 +import Log
    1.10 +begin
    1.11  
    1.12  lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
    1.13  by (induct_tac "n", auto)