--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Dec 29 17:34:41 2010 +0100
@@ -4,7 +4,10 @@
Translation from HOL light: Robert Himmelmann, TU Muenchen *)
theory Integration
- imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
+imports
+ Derivative
+ "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+ "~~/src/HOL/Library/Indicator_Function"
begin
declare [[smt_certificates="Integration.certs"]]