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.*}