equal
deleted
inserted
replaced
36 |
36 |
37 The sos method generates a certificate which can be used to repeat |
37 The sos method generates a certificate which can be used to repeat |
38 the proof without calling an external prover. |
38 the proof without calling an external prover. |
39 *} |
39 *} |
40 |
40 |
41 setup Sum_of_Squares.setup |
|
42 setup SOS_Wrapper.setup |
41 setup SOS_Wrapper.setup |
43 |
42 |
44 text {* Tests *} |
43 text {* Tests *} |
45 |
44 |
46 lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" |
45 lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" |