author | paulson <lp15@cam.ac.uk> |
Tue, 31 Mar 2015 15:00:03 +0100 | |
changeset 59862 | 44b3f4fa33ca |
parent 58881 | b9556a055632 |
child 60500 | 903bb1495239 |
permissions | -rw-r--r-- |
(* Title: HOL/Library/Sum_of_Squares.thy Author: Amine Chaieb, University of Cambridge Author: Philipp Meyer, TU Muenchen *) section {* A decision procedure for universal multivariate real arithmetic with addition, multiplication and ordering using semidefinite programming *} theory Sum_of_Squares imports Complex_Main begin ML_file "positivstellensatz.ML" ML_file "Sum_of_Squares/sum_of_squares.ML" ML_file "Sum_of_Squares/positivstellensatz_tools.ML" ML_file "Sum_of_Squares/sos_wrapper.ML" end