# HG changeset patch
# User huffman
# Date 1230568290 28800
# Node ID 165e959721c21631731a5d78242989d8a43a2236
# Parent  53930d089f8896346f425dbc8b6304c17a6e9f3e
minimize imports

diff -r 53930d089f88 -r 165e959721c2 src/HOL/Integration.thy
--- 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.*}