src/HOL/Library/Sum_Of_Squares.thy
changeset 32271 378ebd64447d
parent 32268 d50f0cb67578
child 32332 bc5cec7b2be6
--- 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.coin-or.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.coin-or.org/Csdp/), put the executable csdp on your path,
-and call it with (sos csdp)
-
-*)
-
 (* setup sos tactic *)
 setup SosWrapper.setup