| changeset 22983 | 3314057c3b57 |
| parent 21782 | bf055d30d3ad |
| child 22985 | 501e6dfe4e5a |
--- a/src/HOL/Hyperreal/MacLaurin.thy Wed May 16 09:45:22 2007 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Wed May 16 23:03:45 2007 +0200 @@ -7,7 +7,7 @@ header{*MacLaurin Series*} theory MacLaurin -imports Log +imports Transcendental begin subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}