src/HOL/Integration.thy
changeset 29469 c03d2db1cda8
parent 29353 3d2e35c23c66
child 29811 026b0f9f579f
--- a/src/HOL/Integration.thy	Mon Jan 12 23:36:30 2009 -0800
+++ b/src/HOL/Integration.thy	Tue Jan 13 06:55:13 2009 -0800
@@ -6,7 +6,7 @@
 header{*Theory of Integration*}
 
 theory Integration
-imports Deriv
+imports Deriv ATP_Linkup
 begin
 
 text{*We follow John Harrison in formalizing the Gauge integral.*}