--- a/src/HOL/Library/Sum_of_Squares.thy Wed Oct 08 10:15:04 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares.thy Wed Oct 08 11:09:17 2014 +0200
@@ -3,8 +3,8 @@
Author: Philipp Meyer, TU Muenchen
*)
-header {* A decision method for universal multivariate real arithmetic with addition,
- multiplication and ordering using semidefinite programming *}
+header {* A decision procedure for universal multivariate real arithmetic
+ with addition, multiplication and ordering using semidefinite programming *}
theory Sum_of_Squares
imports Complex_Main
@@ -15,27 +15,4 @@
ML_file "Sum_of_Squares/positivstellensatz_tools.ML"
ML_file "Sum_of_Squares/sos_wrapper.ML"
-text {*
- Proof method sos invocations:
- \begin{itemize}
-
- \item remote solver: @{text "(sos remote_csdp)"}
-
- \item local solver: @{text "(sos csdp)"}
-
- The latter requires a local executable from
- @{url "https://projects.coin-or.org/Csdp"} and the Isabelle settings variable
- variable @{text ISABELLE_CSDP} pointing to it.
-
- \end{itemize}
-
- By default, method sos calls @{text 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.
-
- The sos method generates a certificate which can be used to repeat
- the proof without calling an external prover.
-*}
-
end