equal
deleted
inserted
replaced
2 header {* Kurzweil-Henstock gauge integration in many dimensions. *} |
2 header {* Kurzweil-Henstock gauge integration in many dimensions. *} |
3 (* Author: John Harrison |
3 (* Author: John Harrison |
4 Translation from HOL light: Robert Himmelmann, TU Muenchen *) |
4 Translation from HOL light: Robert Himmelmann, TU Muenchen *) |
5 |
5 |
6 theory Integration |
6 theory Integration |
7 imports Derivative SMT |
7 imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" |
8 begin |
8 begin |
9 |
9 |
10 declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]] |
10 declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]] |
11 declare [[smt_fixed=true]] |
11 declare [[smt_fixed=true]] |
12 declare [[z3_proofs=true]] |
12 declare [[z3_proofs=true]] |
|
13 |
|
14 setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *} |
|
15 |
13 |
16 |
14 subsection {* Sundries *} |
17 subsection {* Sundries *} |
15 |
18 |
16 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto |
19 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto |
17 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto |
20 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto |