src/HOL/Library/Sum_of_Squares.thy
author wenzelm
Sun Jan 06 15:04:34 2019 +0100 (6 months ago)
changeset 69605 a96320074298
parent 60500 903bb1495239
child 70333 0f7edf0853df
permissions -rw-r--r--
isabelle update -u path_cartouches;
     1 (*  Title:      HOL/Library/Sum_of_Squares.thy
     2     Author:     Amine Chaieb, University of Cambridge
     3     Author:     Philipp Meyer, TU Muenchen
     4 *)
     5 
     6 section \<open>A decision procedure for universal multivariate real arithmetic
     7   with addition, multiplication and ordering using semidefinite programming\<close>
     8 
     9 theory Sum_of_Squares
    10 imports Complex_Main
    11 begin
    12 
    13 ML_file \<open>positivstellensatz.ML\<close>
    14 ML_file \<open>Sum_of_Squares/sum_of_squares.ML\<close>
    15 ML_file \<open>Sum_of_Squares/positivstellensatz_tools.ML\<close>
    16 ML_file \<open>Sum_of_Squares/sos_wrapper.ML\<close>
    17 
    18 end