equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Sum_of_Squares_Remote.thy |
1 (* Title: HOL/Library/Sum_of_Squares_Remote.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 header {* Examples with remote CSDP *} |
6 section {* Examples with remote CSDP *} |
7 |
7 |
8 theory Sum_of_Squares_Remote |
8 theory Sum_of_Squares_Remote |
9 imports Sum_of_Squares |
9 imports Sum_of_Squares |
10 begin |
10 begin |
11 |
11 |