--- a/src/HOL/Integration.thy Mon Dec 29 15:23:56 2008 +0100
+++ b/src/HOL/Integration.thy Mon Dec 29 08:31:30 2008 -0800
@@ -6,7 +6,7 @@
header{*Theory of Integration*}
theory Integration
-imports MacLaurin
+imports Deriv
begin
text{*We follow John Harrison in formalizing the Gauge integral.*}