equal
deleted
inserted
replaced
6 theory Integration |
6 theory Integration |
7 imports Derivative SMT |
7 imports Derivative SMT |
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.cert"]] |
11 declare [[smt_record=false]] |
11 declare [[smt_fixed=true]] |
12 declare [[z3_proofs=true]] |
12 declare [[z3_proofs=true]] |
13 |
13 |
14 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto |
14 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto |
15 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto |
15 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto |
16 lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto |
16 lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto |