equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Sum_of_Squares.thy |
1 (* Title: HOL/Library/Sum_of_Squares.thy |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 Author: Philipp Meyer, TU Muenchen |
3 Author: Philipp Meyer, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 section {* A decision procedure for universal multivariate real arithmetic |
6 section \<open>A decision procedure for universal multivariate real arithmetic |
7 with addition, multiplication and ordering using semidefinite programming *} |
7 with addition, multiplication and ordering using semidefinite programming\<close> |
8 |
8 |
9 theory Sum_of_Squares |
9 theory Sum_of_Squares |
10 imports Complex_Main |
10 imports Complex_Main |
11 begin |
11 begin |
12 |
12 |