# HG changeset patch
# User huffman
# Date 1231858513 28800
# Node ID c03d2db1cda84b2d3405703815b56629bea38f0b
# Parent  b2cfb5d0a59e1c8874727dbfb2e2fea043b98eb8
Integration imports ATP_Linkup (for metis)

diff -r b2cfb5d0a59e -r c03d2db1cda8 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.*}