1.1 --- a/src/HOL/Library/Sum_Of_Squares.thy	Wed Aug 05 17:10:10 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares.thy	Thu Aug 06 19:51:59 2009 +0200
     1.3 @@ -2,9 +2,9 @@
     1.4     Author:     Amine Chaieb, University of Cambridge
     1.5  
     1.6  In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
     1.7 -or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path,
     1.8 -and call it with (sos csdp). By default, sos calls remote_csdp. This can take of the order
     1.9 -of a minute for one sos call, because sos calls CSDP repeatedly.
    1.10 +or install CSDP (https://projects.coin-or.org/Csdp/), set the Isabelle environment
    1.11 +variable CSDP_EXE and call it with (sos csdp). By default, sos calls remote_csdp.
    1.12 +This can take of the order of a minute for one sos call, because sos calls CSDP repeatedly.
    1.13  If you install CSDP locally, sos calls typically takes only a few seconds.
    1.14  
    1.15  *)
    1.16 @@ -13,11 +13,19 @@
    1.17            multiplication and ordering using semidefinite programming*}
    1.18  
    1.19  theory Sum_Of_Squares
    1.20 -  imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
    1.21 -  uses "positivstellensatz.ML" "sum_of_squares.ML" "sos_wrapper.ML"
    1.22 -  begin
    1.23 +imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
    1.24 +uses
    1.25 +  ("positivstellensatz.ML")
    1.26 +  ("Sum_Of_Squares/sum_of_squares.ML")
    1.27 +  ("Sum_Of_Squares/sos_wrapper.ML")
    1.28 +begin
    1.29  
    1.30  (* setup sos tactic *)
    1.31 +
    1.32 +use "positivstellensatz.ML"
    1.33 +use "Sum_Of_Squares/sum_of_squares.ML"
    1.34 +use "Sum_Of_Squares/sos_wrapper.ML"
    1.35 +
    1.36  setup SosWrapper.setup
    1.37  
    1.38  text{* Tests -- commented since they work only when csdp is installed  or take too long with remote csdps *}