# HG changeset patch
# User wenzelm
# Date 1249584393 -7200
# Node ID d4cb904cc63cf1b544eb9e3f50754835784e6cff
# Parent  bc5cec7b2be6519b5d20ae4993f50ee42893a44c
tuned header;
visible text instead of source comments;

diff -r bc5cec7b2be6 -r d4cb904cc63c src/HOL/Library/Sum_Of_Squares.thy
--- a/src/HOL/Library/Sum_Of_Squares.thy	Thu Aug 06 19:51:59 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Thu Aug 06 20:46:33 2009 +0200
@@ -1,26 +1,30 @@
-(* Title:      Library/Sum_Of_Squares
+(* Title:      HOL/Library/Sum_Of_Squares.thy
    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/), set the Isabelle environment
-variable CSDP_EXE 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*}
+  multiplication and ordering using semidefinite programming *}
 
 theory Sum_Of_Squares
 imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
 uses
-  ("positivstellensatz.ML")
+  ("positivstellensatz.ML")  (* duplicate use!? -- cf. Euclidian_Space.thy *)
   ("Sum_Of_Squares/sum_of_squares.ML")
   ("Sum_Of_Squares/sos_wrapper.ML")
 begin
 
-(* setup sos tactic *)
+text {*
+  In order to use the method sos, call it with @{text "(sos
+  remote_csdp)"} to use the remote solver.  Or install CSDP
+  (https://projects.coin-or.org/Csdp), configure the Isabelle setting
+  @{text CSDP_EXE}, and call it with @{text "(sos csdp)"}.  By
+  default, 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.
+*}
+
+text {* setup sos tactic *}
 
 use "positivstellensatz.ML"
 use "Sum_Of_Squares/sum_of_squares.ML"
@@ -28,7 +32,8 @@
 
 setup SosWrapper.setup
 
-text{* Tests -- commented since they work only when csdp is installed  or take too long with remote csdps *}
+text {* Tests -- commented since they work only when csdp is installed
+  or take too long with remote csdps *}
 
 (*
 lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos