# HG changeset patch
# User nipkow
# Date 1248862401 7200
# Node ID 378ebd64447dc202838b6c46cc6f88d7f7ca4c0f
# Parent 615c524bd9e4dfde6b8f4e75d649b5384ac5fbdc
sos comments modified
diff r 615c524bd9e4 r 378ebd64447d src/HOL/Library/Sum_Of_Squares.thy
 a/src/HOL/Library/Sum_Of_Squares.thy Wed Jul 29 12:12:01 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy Wed Jul 29 12:13:21 2009 +0200
@@ 1,22 +1,22 @@
(* Title: Library/Sum_Of_Squares
Author: Amine Chaieb, University of Cambridge
+
+In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
+or install CSDP (https://projects.coinor.org/Csdp/), put the executable csdp on your path,
+and call it with (sos csdp). By default, sos calls remote_csdp. This can take of the order
+of a minute for one sos call, because sos calls CSDP repeatedly.
+If you install CSDP locally, sos calls typically takes only a few seconds.
+
*)
header {* A decision method for universal multivariate real arithmetic with addition,
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" "sos_wrapper.ML"
begin
(* Note:

In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
or install CSDP (https://projects.coinor.org/Csdp/), put the executable csdp on your path,
and call it with (sos csdp)

*)

(* setup sos tactic *)
setup SosWrapper.setup