src/HOL/Library/Sum_Of_Squares.thy
changeset 31512 27118561c2e0
parent 31131 d9752181691a
child 32268 d50f0cb67578
     1.1 --- a/src/HOL/Library/Sum_Of_Squares.thy	Mon Jun 08 22:29:37 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares.thy	Tue Jun 09 11:10:33 2009 +0200
     1.3 @@ -15,12 +15,10 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -
     1.8  method_setup sos = {* Scan.succeed (SIMPLE_METHOD' o Sos.sos_tac) *} 
     1.9    "Prove universal problems over the reals using sums of squares"
    1.10  
    1.11  text{* Tests -- commented since they work only when csdp is installed -- see above *}
    1.12 -
    1.13  (*
    1.14  lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
    1.15  
    1.16 @@ -59,8 +57,8 @@
    1.17  (* ------------------------------------------------------------------------- *)
    1.18  (*
    1.19  lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
    1.20 +*)
    1.21  
    1.22 -*)
    1.23  (* ------------------------------------------------------------------------- *)
    1.24  (* Inequality from sci.math (see "Leon-Sotelo, por favor").                  *)
    1.25  (* ------------------------------------------------------------------------- *)