--- a/src/HOL/Library/Sum_Of_Squares.thy Fri Jul 24 11:31:22 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy Fri Jul 24 13:56:02 2009 +0200
@@ -6,19 +6,22 @@
multiplication and ordering using semidefinite programming*}
theory Sum_Of_Squares
imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
- uses "positivstellensatz.ML" "sum_of_squares.ML"
+ uses "positivstellensatz.ML" "sum_of_squares.ML" "sos_wrapper.ML"
begin
(* Note:
-In order to use the method sos, install CSDP (https://projects.coin-or.org/Csdp/) and put the executable csdp on your path.
+In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
+or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path,
+and call it with (sos csdp)
*)
-method_setup sos = {* Scan.succeed (SIMPLE_METHOD' o Sos.sos_tac) *}
- "Prove universal problems over the reals using sums of squares"
+(* setup sos tactic *)
+setup SosWrapper.setup
-text{* Tests -- commented since they work only when csdp is installed -- see above *}
+text{* Tests -- commented since they work only when csdp is installed or take too long with remote csdps *}
+
(*
lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
@@ -115,3 +118,4 @@
*)
end
+