--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed May 12 23:54:02 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed May 12 23:54:04 2010 +0200
@@ -4,13 +4,16 @@
Translation from HOL light: Robert Himmelmann, TU Muenchen *)
theory Integration
- imports Derivative SMT
+ imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
begin
-declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
+declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]]
declare [[smt_fixed=true]]
declare [[z3_proofs=true]]
+setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
+
+
subsection {* Sundries *}
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto