sos comments modified
authornipkow
Wed Jul 29 12:13:21 2009 +0200 (2009-07-29)
changeset 32271378ebd64447d
parent 32270 615c524bd9e4
child 32274 e7f275d203bc
sos comments modified
src/HOL/Library/Sum_Of_Squares.thy
     1.1 --- a/src/HOL/Library/Sum_Of_Squares.thy	Wed Jul 29 12:12:01 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares.thy	Wed Jul 29 12:13:21 2009 +0200
     1.3 @@ -1,22 +1,22 @@
     1.4  (* Title:      Library/Sum_Of_Squares
     1.5     Author:     Amine Chaieb, University of Cambridge
     1.6 +
     1.7 +In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
     1.8 +or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path,
     1.9 +and call it with (sos csdp). By default, sos calls remote_csdp. This can take of the order
    1.10 +of a minute for one sos call, because sos calls CSDP repeatedly.
    1.11 +If you install CSDP locally, sos calls typically takes only a few seconds.
    1.12 +
    1.13  *)
    1.14  
    1.15  header {* A decision method for universal multivariate real arithmetic with addition, 
    1.16            multiplication and ordering using semidefinite programming*}
    1.17 +
    1.18  theory Sum_Of_Squares
    1.19    imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
    1.20    uses "positivstellensatz.ML" "sum_of_squares.ML" "sos_wrapper.ML"
    1.21    begin
    1.22  
    1.23 -(* Note: 
    1.24 -
    1.25 -In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
    1.26 -or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path,
    1.27 -and call it with (sos csdp)
    1.28 -
    1.29 -*)
    1.30 -
    1.31  (* setup sos tactic *)
    1.32  setup SosWrapper.setup
    1.33