equal
deleted
inserted
replaced
5 |
5 |
6 theory Integration |
6 theory Integration |
7 imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function |
7 imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function |
8 begin |
8 begin |
9 |
9 |
10 declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]] |
10 declare [[smt_certificates="Integration.certs"]] |
11 declare [[smt_fixed=true]] |
11 declare [[smt_fixed=true]] |
12 declare [[smt_oracle=false]] |
12 declare [[smt_oracle=false]] |
13 |
13 |
14 setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *} |
14 setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *} |
15 |
15 |