Integration imports ATP_Linkup (for metis)
authorhuffman
Tue, 13 Jan 2009 06:55:13 -0800
changeset 29469 c03d2db1cda8
parent 29465 b2cfb5d0a59e
child 29470 1851088a1f87
Integration imports ATP_Linkup (for metis)
src/HOL/Integration.thy
--- 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.*}