author  wenzelm 
Wed, 17 Jun 2015 11:03:05 +0200  
changeset 60500  903bb1495239 
parent 58881  b9556a055632 
child 69605  a96320074298 
permissions  rwrr 
41474  1 
(* Title: HOL/Library/Sum_of_Squares.thy 
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32645
diff
changeset

2 
Author: Amine Chaieb, University of Cambridge 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32645
diff
changeset

3 
Author: Philipp Meyer, TU Muenchen 
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset

4 
*) 
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset

5 

60500  6 
section \<open>A decision procedure for universal multivariate real arithmetic 
7 
with addition, multiplication and ordering using semidefinite programming\<close> 

32271  8 

41474  9 
theory Sum_of_Squares 
38136  10 
imports Complex_Main 
32332  11 
begin 
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset

12 

48891  13 
ML_file "positivstellensatz.ML" 
14 
ML_file "Sum_of_Squares/sum_of_squares.ML" 

15 
ML_file "Sum_of_Squares/positivstellensatz_tools.ML" 

16 
ML_file "Sum_of_Squares/sos_wrapper.ML" 

17 

31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset

18 
end 